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)

@[implicit_reducible]

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.

@[implicit_reducible]

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.

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.

theorem tendsto_pow_cobounded_cobounded {α : Type u_1} [SeminormedRing α] [NormOneClass α] [NormMulClass α] {m : ℕ} (hm : m ≠ 0) : Filter.Tendsto (fun (x : α) => x ^ m) (Bornology.cobounded α) (Bornology.cobounded α)

@[implicit_reducible]

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.

@[implicit_reducible]

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.

@[implicit_reducible]

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.

@[implicit_reducible]

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.

@[implicit_reducible]

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.

@[implicit_reducible]

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.

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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

@[implicit_reducible]

instance Int.instNormedCommRing : NormedCommRing ℤ

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.

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

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