Normed additive commutative groups of rings

This file contains the NormedAddCommGroupOfRing class, which bundles the ring structure together with the normed additive commutative group structure.

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

A ring whose additive group is a normed additive commutative group.

• 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
• 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
• npow : ℕ → B → B
• npow_zero (x : B) : Monoid.npow 0 x = 1
• npow_succ (n : ℕ) (x : B) : Monoid.npow (n + 1) x = Monoid.npow n x * x
• zero_mul (a : B) : 0 * a = 0
• mul_zero (a : B) : a * 0 = 0
• 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
• natCast : ℕ → B
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• 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

The algebra structure coming from compatible scalar multiplication and multiplication.

Equations

• Algebra.ofIsScalarTowerSmulCommClass = Algebra.ofModule ⋯ ⋯

@[reducible]

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

The pointwise ring with the L^2 product norm is a normed additive group of rings.

Equations

• PiNormedAddCommGroupOfRing = { toRing := Pi.ring, toNorm := (PiLp.normedAddCommGroupToPi 2 B).toNorm, toMetricSpace := (PiLp.normedAddCommGroupToPi 2 B).toMetricSpace, dist_eq := ⋯ }

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)

The L^2 norm on a finite product is the square root of the sum of squared norms.