Normed additive commutative groups of rings #
This file contains the definition of normed_add_comm_group_of_ring which is a structure
combining the ring structure, the norm, and the metric space structure.
@[class]
- to_has_norm : has_norm B
- to_ring : ring B
- to_metric_space : metric_space B
- dist_eq : (∀ (x y : B), has_dist.dist x y = ‖x - y‖) . "obviously"
normed_add_comm_group structure extended by ring
Instances of this typeclass
Instances of other typeclasses for normed_add_comm_group_of_ring
- normed_add_comm_group_of_ring.has_sizeof_inst
@[instance]
def
normed_add_comm_group_of_ring.to_normed_add_comm_group
{B : Type u_1}
[h : normed_add_comm_group_of_ring B] :
Equations
- normed_add_comm_group_of_ring.to_normed_add_comm_group = {to_has_norm := normed_add_comm_group_of_ring.to_has_norm h, to_add_comm_group := non_unital_non_assoc_ring.to_add_comm_group B (non_assoc_ring.to_non_unital_non_assoc_ring B), to_metric_space := normed_add_comm_group_of_ring.to_metric_space h, dist_eq := _}
def
algebra.of_is_scalar_tower_smul_comm_class
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[semiring A]
[module R A]
[smul_comm_class R A A]
[is_scalar_tower R A A] :
algebra R A
Equations
- algebra.of_is_scalar_tower_smul_comm_class = algebra.of_module algebra.of_is_scalar_tower_smul_comm_class._proof_1 algebra.of_is_scalar_tower_smul_comm_class._proof_2
@[protected, instance]
noncomputable
def
pi.normed_add_comm_group_of_ring
{ι : Type u_1}
[fintype ι]
{B : ι → Type u_2}
[Π (i : ι), normed_add_comm_group_of_ring (B i)] :
normed_add_comm_group_of_ring (Π (i : ι), B i)
Equations
- pi.normed_add_comm_group_of_ring = {to_has_norm := pi_Lp.has_norm 2 B (λ (i : ι), mul_zero_class.to_has_zero (B i)), to_ring := pi.ring (λ (i : ι), normed_add_comm_group_of_ring.to_ring), to_metric_space := pi_Lp.metric_space 2 B (λ (i : ι), normed_add_comm_group_of_ring.to_metric_space), dist_eq := _}