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} {R : ι → Type u_4} [Fintype ι] [(i : ι) → NonUnitalSeminormedRing (R i)] : NonUnitalSeminormedRing ((i : ι) → R i)

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

theorem RingHom.isometry {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} [SeminormedRing 𝕜₁] [SeminormedRing 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) [RingHomIsometric σ] : Isometry ⇑σ

theorem RingHomIsometric.inv {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} [SeminormedRing 𝕜₁] [SeminormedRing 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {σ' : 𝕜₂ →+* 𝕜₁} [RingHomInvPair σ σ'] [RingHomIsometric σ] : RingHomIsometric σ'

If σ and σ' are mutually inverse, then one is RingHomIsometric if the other is. Not an instance, as it would cause loops.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

instance Pi.nonUnitalSeminormedCommRing {ι : Type u_3} {R : ι → Type u_4} [Fintype ι] [(i : ι) → NonUnitalSeminormedCommRing (R i)] : NonUnitalSeminormedCommRing ((i : ι) → R 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 = { toNonUnitalSeminormedRing := Pi.nonUnitalSeminormedRing, mul_comm := ⋯ }

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

@[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 = { toNorm := inferInstance.toNorm, toNonUnitalRing := inferInstance, toMetricSpace := inferInstance.toMetricSpace, dist_eq := ⋯, norm_mul_le := ⋯ }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• SeparationQuotient.instNormedRing = { toNorm := inferInstance.toNorm, toRing := inferInstance, toMetricSpace := inferInstance.toMetricSpace, dist_eq := ⋯, norm_mul_le := ⋯ }

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

Equations

• One or more equations did not get rendered due to their size.

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

• One or more equations did not get rendered due to their size.

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