Normed rings

In this file we continue building the theory of (semi)normed rings.

theorem Filter.Tendsto.zero_mul_isBoundedUnder_le {α : Type u_1} {ι : Type u_3} [NonUnitalSeminormedRing α] {f g : ι → α} {l : Filter ι} (hf : Tendsto f l (nhds 0)) (hg : IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l ((fun (x : α) => ‖x‖) ∘ g)) : Tendsto (fun (x : ι) => f x * g x) l (nhds 0)

theorem Filter.isBoundedUnder_le_mul_tendsto_zero {α : Type u_1} {ι : Type u_3} [NonUnitalSeminormedRing α] {f g : ι → α} {l : Filter ι} (hf : IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l (norm ∘ f)) (hg : Tendsto g l (nhds 0)) : Tendsto (fun (x : ι) => f x * g x) l (nhds 0)

instance Pi.nonUnitalSeminormedRing {ι : Type u_3} {π : ι → Type u_4} [Fintype ι] [(i : ι) → NonUnitalSeminormedRing (π i)] : NonUnitalSeminormedRing ((i : ι) → π i)

Non-unital seminormed ring structure on the product of finitely many non-unital seminormed rings, using the sup norm.

Equations

• Pi.nonUnitalSeminormedRing = NonUnitalSeminormedRing.mk ⋯ ⋯

instance Pi.seminormedRing {ι : Type u_3} {π : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedRing (π i)] : SeminormedRing ((i : ι) → π i)

Seminormed ring structure on the product of finitely many seminormed rings, using the sup norm.

Equations

• Pi.seminormedRing = SeminormedRing.mk ⋯ ⋯

instance Pi.nonUnitalNormedRing {ι : Type u_3} {π : ι → Type u_4} [Fintype ι] [(i : ι) → NonUnitalNormedRing (π i)] : NonUnitalNormedRing ((i : ι) → π i)

Normed ring structure on the product of finitely many non-unital normed rings, using the sup norm.

Equations

• Pi.nonUnitalNormedRing = NonUnitalNormedRing.mk ⋯ ⋯

instance Pi.normedRing {ι : Type u_3} {π : ι → Type u_4} [Fintype ι] [(i : ι) → NormedRing (π i)] : NormedRing ((i : ι) → π i)

Normed ring structure on the product of finitely many normed rings, using the sup norm.

Equations

• Pi.normedRing = NormedRing.mk ⋯ ⋯

instance Pi.nonUnitalSeminormedCommRing {ι : Type u_3} {π : ι → Type u_4} [Fintype ι] [(i : ι) → NonUnitalSeminormedCommRing (π i)] : NonUnitalSeminormedCommRing ((i : ι) → π i)

Non-unital seminormed commutative ring structure on the product of finitely many non-unital seminormed commutative rings, using the sup norm.

Equations

• Pi.nonUnitalSeminormedCommRing = NonUnitalSeminormedCommRing.mk ⋯

instance Pi.nonUnitalNormedCommRing {ι : Type u_3} {π : ι → Type u_4} [Fintype ι] [(i : ι) → NonUnitalNormedCommRing (π i)] : NonUnitalNormedCommRing ((i : ι) → π i)

Normed commutative ring structure on the product of finitely many non-unital normed commutative rings, using the sup norm.

Equations

• Pi.nonUnitalNormedCommRing = NonUnitalNormedCommRing.mk ⋯

instance Pi.seminormedCommRing {ι : Type u_3} {π : ι → Type u_4} [Fintype ι] [(i : ι) → SeminormedCommRing (π i)] : SeminormedCommRing ((i : ι) → π i)

Seminormed commutative ring structure on the product of finitely many seminormed commutative rings, using the sup norm.

Equations

• Pi.seminormedCommRing = SeminormedCommRing.mk ⋯

instance Pi.normedCommutativeRing {ι : Type u_3} {π : ι → Type u_4} [Fintype ι] [(i : ι) → NormedCommRing (π i)] : NormedCommRing ((i : ι) → π i)

Normed commutative ring structure on the product of finitely many normed commutative rings, using the sup norm.

Equations

• Pi.normedCommutativeRing = NormedCommRing.mk ⋯

@[instance 100]

instance NonUnitalSeminormedRing.toContinuousMul {α : Type u_1} [NonUnitalSeminormedRing α] : ContinuousMul α

@[instance 100]

instance NonUnitalSeminormedRing.toIsTopologicalRing {α : Type u_1} [NonUnitalSeminormedRing α] : IsTopologicalRing α

A seminormed ring is a topological ring.

instance SeparationQuotient.instNonUnitalNormedRing {α : Type u_1} [NonUnitalSeminormedRing α] : NonUnitalNormedRing (SeparationQuotient α)

Equations

• SeparationQuotient.instNonUnitalNormedRing = NonUnitalNormedRing.mk ⋯ ⋯

instance SeparationQuotient.instNonUnitalNormedCommRing {α : Type u_1} [NonUnitalSeminormedCommRing α] : NonUnitalNormedCommRing (SeparationQuotient α)

Equations

• SeparationQuotient.instNonUnitalNormedCommRing = NonUnitalNormedCommRing.mk ⋯

instance SeparationQuotient.instNormedRing {α : Type u_1} [SeminormedRing α] : NormedRing (SeparationQuotient α)

Equations

• SeparationQuotient.instNormedRing = NormedRing.mk ⋯ ⋯

instance SeparationQuotient.instNormedCommRing {α : Type u_1} [SeminormedCommRing α] : NormedCommRing (SeparationQuotient α)

Equations

• SeparationQuotient.instNormedCommRing = NormedCommRing.mk ⋯

instance SeparationQuotient.instNormOneClass {α : Type u_1} [SeminormedAddCommGroup α] [One α] [NormOneClass α] : NormOneClass (SeparationQuotient α)

theorem NNReal.lipschitzWith_sub : LipschitzWith 2 fun (p : NNReal × NNReal) => p.1 - p.2

instance Int.instNormedCommRing : NormedCommRing ℤ

Equations

• Int.instNormedCommRing = NormedCommRing.mk ⋯

instance Int.instNormOneClass : NormOneClass ℤ