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 ℤ

instance Int.instNormMulClass : NormMulClass ℤ

theorem antilipschitzWith_mul_left {α : Type u_1} [NonUnitalNormedRing α] [NormMulClass α] {a : α} (ha : a ≠ 0) : AntilipschitzWith ‖a‖₊⁻¹ fun (x : α) => a * x

theorem antilipschitzWith_mul_right {α : Type u_1} [NonUnitalNormedRing α] [NormMulClass α] {a : α} (ha : a ≠ 0) : AntilipschitzWith ‖a‖₊⁻¹ fun (x : α) => x * a

def Dilation.mulLeft {α : Type u_1} [NonUnitalNormedRing α] [NormMulClass α] (a : α) (ha : a ≠ 0) : α →ᵈ α

Multiplication by a nonzero element a on the left, as a Dilation of a ring with a strictly multiplicative norm.

Equations

• Dilation.mulLeft a ha = { toFun := fun (b : α) => a * b, edist_eq' := ⋯ }

@[simp]

theorem Dilation.mulLeft_toFun {α : Type u_1} [NonUnitalNormedRing α] [NormMulClass α] (a : α) (ha : a ≠ 0) (b : α) : (mulLeft a ha) b = a * b

def Dilation.mulRight {α : Type u_1} [NonUnitalNormedRing α] [NormMulClass α] (a : α) (ha : a ≠ 0) : α →ᵈ α

Multiplication by a nonzero element a on the right, as a Dilation of a ring with a strictly multiplicative norm.

Equations

• Dilation.mulRight a ha = { toFun := fun (b : α) => b * a, edist_eq' := ⋯ }

@[simp]

theorem Dilation.mulRight_toFun {α : Type u_1} [NonUnitalNormedRing α] [NormMulClass α] (a : α) (ha : a ≠ 0) (b : α) : (mulRight a ha) b = b * a

@[simp]

theorem Filter.comap_mul_left_cobounded {α : Type u_1} [NonUnitalNormedRing α] [NormMulClass α] {a : α} (ha : a ≠ 0) : comap (fun (x : α) => a * x) (Bornology.cobounded α) = Bornology.cobounded α

@[simp]

theorem Filter.comap_mul_right_cobounded {α : Type u_1} [NonUnitalNormedRing α] [NormMulClass α] {a : α} (ha : a ≠ 0) : comap (fun (x : α) => x * a) (Bornology.cobounded α) = Bornology.cobounded α

theorem IsOfFinOrder.norm_eq_one {α : Type u_1} [NormedRing α] [NormMulClass α] [NormOneClass α] {a : α} (ha : IsOfFinOrder a) : ‖a‖ = 1

@[simp]

theorem AddChar.norm_apply {α : Type u_1} [NormedRing α] [NormMulClass α] [NormOneClass α] {G : Type u_4} [AddLeftCancelMonoid G] [Finite G] (ψ : AddChar G α) (x : G) : ‖ψ x‖ = 1