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 , NormedAddCommGroup , Semiring , Norm , AddCommGroup , AddGroupWithOne , NonUnitalSemiring , NonAssocSemiring , MonoidWithZero , NonUnitalNonAssocSemiring , Monoid , MulZeroOneClass , SemigroupWithZero , AddCommMonoidWithOne , MulOneClass , IntCast , AddMonoidWithOne , MetricSpace , AddGroup , AddCommMonoid , Distrib , Semigroup , MulZeroClass , NatCast , SubNegMonoid , AddMonoid , One , Neg , Sub , AddCommSemigroup , AddSemigroup , AddZeroClass , Mul , Zero , AddCommMagma , Add , PseudoMetricSpace , Dist : Type u_1

normed_add_comm_group structure extended by ring

@[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)