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.

@[reducible]

class NormedAddCommGroupOfRing (B : Type u_1) extends Ring B, NormedAddCommGroup B : Type u_1

normed_add_comm_group structure extended by ring

• add : B → B → B
• add_assoc (a b c : B) : a + b + c = a + (b + c)
• zero : B
• zero_add (a : B) : 0 + a = a
• add_zero (a : B) : a + 0 = a
• nsmul : ℕ → B → B
• nsmul_zero (x : B) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : B) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : B) : a + b = b + a
• mul : B → B → B
• left_distrib (a b c : B) : a * (b + c) = a * b + a * c
• right_distrib (a b c : B) : (a + b) * c = a * c + b * c
• zero_mul (a : B) : 0 * a = 0
• mul_zero (a : B) : a * 0 = 0
• mul_assoc (a b c : B) : a * b * c = a * (b * c)
• one : B
• one_mul (a : B) : 1 * a = a
• mul_one (a : B) : a * 1 = a
• natCast : ℕ → B
• natCast_zero : NatCast.natCast 0 = 0
• natCast_succ (n : ℕ) : NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → B → B
• npow_zero (x : B) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : B) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : B → B
• sub : B → B → B
• sub_eq_add_neg (a b : B) : a - b = a + -b
• zsmul : ℤ → B → B
• zsmul_zero' (a : B) : Ring.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : B) : Ring.zsmul (↑n.succ) a = Ring.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : B) : Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• neg_add_cancel (a : B) : -a + a = 0
• intCast : ℤ → B
• intCast_ofNat (n : ℕ) : IntCast.intCast ↑n = ↑n
• intCast_negSucc (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• norm : B → ℝ
• dist : B → B → ℝ
• dist_self (x : B) : dist x x = 0
• dist_comm (x y : B) : dist x y = dist y x
• dist_triangle (x y z : B) : dist x z ≤ dist x y + dist y z
• edist : B → B → ENNReal
• edist_dist (x y : B) : edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace B
• uniformity_dist : uniformity B = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : B × B | dist p.1 p.2 < ε}
• toBornology : Bornology B
• cobounded_sets : (Bornology.cobounded B).sets = {s : Set B | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• eq_of_dist_eq_zero {x y : B} : dist x y = 0 → x = y
• dist_eq (x y : B) : dist x y = ‖x - y‖

@[reducible]

def Algebra.ofIsScalarTowerSmulCommClass {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] : Algebra R A

Equations

• Algebra.ofIsScalarTowerSmulCommClass = Algebra.ofModule ⋯ ⋯

noncomputable instance PiNormedAddCommGroupOfRing {ι : Type u_1} [Fintype ι] {B : ι → Type u_2} [(i : ι) → NormedAddCommGroupOfRing (B i)] : NormedAddCommGroupOfRing ((i : ι) → B i)

Equations

• PiNormedAddCommGroupOfRing = NormedAddCommGroupOfRing.mk ⋯

theorem Pi.normedAddCommGroupOfRing.norm_eq_sum {ι : Type u_1} [Fintype ι] {B : ι → Type u_2} [(i : ι) → NormedAddCommGroupOfRing (B i)] (x : (i : ι) → B i) : ‖x‖ = √(∑ i : ι, ‖x i‖ ^ 2)