Normed fields #
In this file we define (semi)normed rings and fields. We also prove some theorems about these definitions.
Some useful results that relate the topology of the normed field to the discrete topology include:
A non-unital seminormed ring is a not-necessarily-unital ring
endowed with a seminorm which satisfies the inequality ‖x y‖ ≤ ‖x‖ ‖y‖
.
- norm : α → ℝ
- add : α → α → α
- zero : α
- nsmul : ℕ → α → α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- neg : α → α
- sub : α → α → α
- zsmul : ℤ → α → α
- zsmul_zero' : ∀ (a : α), SubNegMonoid.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (Int.ofNat n.succ) a = SubNegMonoid.zsmul (Int.ofNat n) a + a
- zsmul_neg' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
- mul : α → α → α
- dist : α → α → ℝ
- edist : α → α → ENNReal
- edist_dist : ∀ (x y : α), PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
- toUniformSpace : UniformSpace α
- uniformity_dist : uniformity α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
- toBornology : Bornology α
The distance is induced by the norm.
The norm is submultiplicative.
Instances
The distance is induced by the norm.
A seminormed ring is a ring endowed with a seminorm which satisfies the inequality
‖x y‖ ≤ ‖x‖ ‖y‖
.
- norm : α → ℝ
- add : α → α → α
- zero : α
- nsmul : ℕ → α → α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- mul : α → α → α
- one : α
- natCast : ℕ → α
- natCast_zero : NatCast.natCast 0 = 0
- natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
- npow : ℕ → α → α
- npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = Semiring.npow n x * x
- neg : α → α
- sub : α → α → α
- zsmul : ℤ → α → α
- zsmul_zero' : ∀ (a : α), Ring.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul (Int.ofNat n) a + a
- zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
- intCast : ℤ → α
- intCast_ofNat : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
- intCast_negSucc : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
- dist : α → α → ℝ
- edist : α → α → ENNReal
- edist_dist : ∀ (x y : α), PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
- toUniformSpace : UniformSpace α
- uniformity_dist : uniformity α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
- toBornology : Bornology α
The distance is induced by the norm.
The norm is submultiplicative.
Instances
The distance is induced by the norm.
A seminormed ring is a non-unital seminormed ring.
Equations
- SeminormedRing.toNonUnitalSeminormedRing = NonUnitalSeminormedRing.mk ⋯ ⋯
A non-unital normed ring is a not-necessarily-unital ring
endowed with a norm which satisfies the inequality ‖x y‖ ≤ ‖x‖ ‖y‖
.
- norm : α → ℝ
- add : α → α → α
- zero : α
- nsmul : ℕ → α → α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- neg : α → α
- sub : α → α → α
- zsmul : ℤ → α → α
- zsmul_zero' : ∀ (a : α), SubNegMonoid.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (Int.ofNat n.succ) a = SubNegMonoid.zsmul (Int.ofNat n) a + a
- zsmul_neg' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
- mul : α → α → α
- dist : α → α → ℝ
- edist : α → α → ENNReal
- edist_dist : ∀ (x y : α), PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
- toUniformSpace : UniformSpace α
- uniformity_dist : uniformity α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
- toBornology : Bornology α
The distance is induced by the norm.
The norm is submultiplicative.
Instances
The distance is induced by the norm.
A non-unital normed ring is a non-unital seminormed ring.
Equations
- NonUnitalNormedRing.toNonUnitalSeminormedRing = NonUnitalSeminormedRing.mk ⋯ ⋯
A normed ring is a ring endowed with a norm which satisfies the inequality ‖x y‖ ≤ ‖x‖ ‖y‖
.
- norm : α → ℝ
- add : α → α → α
- zero : α
- nsmul : ℕ → α → α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- mul : α → α → α
- one : α
- natCast : ℕ → α
- natCast_zero : NatCast.natCast 0 = 0
- natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
- npow : ℕ → α → α
- npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = Semiring.npow n x * x
- neg : α → α
- sub : α → α → α
- zsmul : ℤ → α → α
- zsmul_zero' : ∀ (a : α), Ring.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul (Int.ofNat n) a + a
- zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
- intCast : ℤ → α
- intCast_ofNat : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
- intCast_negSucc : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
- dist : α → α → ℝ
- edist : α → α → ENNReal
- edist_dist : ∀ (x y : α), PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
- toUniformSpace : UniformSpace α
- uniformity_dist : uniformity α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
- toBornology : Bornology α
The distance is induced by the norm.
The norm is submultiplicative.
Instances
The distance is induced by the norm.
A normed division ring is a division ring endowed with a seminorm which satisfies the equality
‖x y‖ = ‖x‖ ‖y‖
.
- norm : α → ℝ
- add : α → α → α
- zero : α
- nsmul : ℕ → α → α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- mul : α → α → α
- one : α
- natCast : ℕ → α
- natCast_zero : NatCast.natCast 0 = 0
- natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
- npow : ℕ → α → α
- npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = Semiring.npow n x * x
- neg : α → α
- sub : α → α → α
- zsmul : ℤ → α → α
- zsmul_zero' : ∀ (a : α), Ring.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul (Int.ofNat n) a + a
- zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
- intCast : ℤ → α
- intCast_ofNat : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
- intCast_negSucc : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
- inv : α → α
- div : α → α → α
- zpow : ℤ → α → α
- zpow_zero' : ∀ (a : α), DivisionRing.zpow 0 a = 1
- zpow_succ' : ∀ (n : ℕ) (a : α), DivisionRing.zpow (Int.ofNat n.succ) a = DivisionRing.zpow (Int.ofNat n) a * a
- zpow_neg' : ∀ (n : ℕ) (a : α), DivisionRing.zpow (Int.negSucc n) a = (DivisionRing.zpow (↑n.succ) a)⁻¹
- exists_pair_ne : ∃ (x : α) (y : α), x ≠ y
- nnratCast : ℚ≥0 → α
- ratCast : ℚ → α
- nnqsmul : ℚ≥0 → α → α
- nnqsmul_def : ∀ (q : ℚ≥0) (a : α), DivisionRing.nnqsmul q a = ↑q * a
- qsmul : ℚ → α → α
- qsmul_def : ∀ (a : ℚ) (x : α), DivisionRing.qsmul a x = ↑a * x
- dist : α → α → ℝ
- edist : α → α → ENNReal
- edist_dist : ∀ (x y : α), PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
- toUniformSpace : UniformSpace α
- uniformity_dist : uniformity α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
- toBornology : Bornology α
The distance is induced by the norm.
The norm is multiplicative.
Instances
The distance is induced by the norm.
A normed division ring is a normed ring.
Equations
- NormedDivisionRing.toNormedRing = NormedRing.mk ⋯ ⋯
A normed ring is a seminormed ring.
Equations
- NormedRing.toSeminormedRing = SeminormedRing.mk ⋯ ⋯
A normed ring is a non-unital normed ring.
Equations
- NormedRing.toNonUnitalNormedRing = NonUnitalNormedRing.mk ⋯ ⋯
A non-unital seminormed commutative ring is a non-unital commutative ring endowed with a
seminorm which satisfies the inequality ‖x y‖ ≤ ‖x‖ ‖y‖
.
- norm : α → ℝ
- add : α → α → α
- zero : α
- nsmul : ℕ → α → α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- neg : α → α
- sub : α → α → α
- zsmul : ℤ → α → α
- zsmul_zero' : ∀ (a : α), SubNegMonoid.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (Int.ofNat n.succ) a = SubNegMonoid.zsmul (Int.ofNat n) a + a
- zsmul_neg' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
- mul : α → α → α
- dist : α → α → ℝ
- edist : α → α → ENNReal
- edist_dist : ∀ (x y : α), PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
- toUniformSpace : UniformSpace α
- uniformity_dist : uniformity α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
- toBornology : Bornology α
Multiplication is commutative.
Instances
Multiplication is commutative.
A non-unital normed commutative ring is a non-unital commutative ring endowed with a
norm which satisfies the inequality ‖x y‖ ≤ ‖x‖ ‖y‖
.
- norm : α → ℝ
- add : α → α → α
- zero : α
- nsmul : ℕ → α → α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- neg : α → α
- sub : α → α → α
- zsmul : ℤ → α → α
- zsmul_zero' : ∀ (a : α), SubNegMonoid.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (Int.ofNat n.succ) a = SubNegMonoid.zsmul (Int.ofNat n) a + a
- zsmul_neg' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
- mul : α → α → α
- dist : α → α → ℝ
- edist : α → α → ENNReal
- edist_dist : ∀ (x y : α), PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
- toUniformSpace : UniformSpace α
- uniformity_dist : uniformity α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
- toBornology : Bornology α
Multiplication is commutative.
Instances
Multiplication is commutative.
A non-unital normed commutative ring is a non-unital seminormed commutative ring.
Equations
- NonUnitalNormedCommRing.toNonUnitalSeminormedCommRing = NonUnitalSeminormedCommRing.mk ⋯
A seminormed commutative ring is a commutative ring endowed with a seminorm which satisfies
the inequality ‖x y‖ ≤ ‖x‖ ‖y‖
.
- norm : α → ℝ
- add : α → α → α
- zero : α
- nsmul : ℕ → α → α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- mul : α → α → α
- one : α
- natCast : ℕ → α
- natCast_zero : NatCast.natCast 0 = 0
- natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
- npow : ℕ → α → α
- npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = Semiring.npow n x * x
- neg : α → α
- sub : α → α → α
- zsmul : ℤ → α → α
- zsmul_zero' : ∀ (a : α), Ring.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul (Int.ofNat n) a + a
- zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
- intCast : ℤ → α
- intCast_ofNat : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
- intCast_negSucc : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
- dist : α → α → ℝ
- edist : α → α → ENNReal
- edist_dist : ∀ (x y : α), PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
- toUniformSpace : UniformSpace α
- uniformity_dist : uniformity α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
- toBornology : Bornology α
Multiplication is commutative.
Instances
Multiplication is commutative.
A normed commutative ring is a commutative ring endowed with a norm which satisfies
the inequality ‖x y‖ ≤ ‖x‖ ‖y‖
.
- norm : α → ℝ
- add : α → α → α
- zero : α
- nsmul : ℕ → α → α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- mul : α → α → α
- one : α
- natCast : ℕ → α
- natCast_zero : NatCast.natCast 0 = 0
- natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
- npow : ℕ → α → α
- npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = Semiring.npow n x * x
- neg : α → α
- sub : α → α → α
- zsmul : ℤ → α → α
- zsmul_zero' : ∀ (a : α), Ring.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul (Int.ofNat n) a + a
- zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
- intCast : ℤ → α
- intCast_ofNat : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
- intCast_negSucc : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
- dist : α → α → ℝ
- edist : α → α → ENNReal
- edist_dist : ∀ (x y : α), PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
- toUniformSpace : UniformSpace α
- uniformity_dist : uniformity α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
- toBornology : Bornology α
Multiplication is commutative.
Instances
Multiplication is commutative.
A seminormed commutative ring is a non-unital seminormed commutative ring.
Equations
- SeminormedCommRing.toNonUnitalSeminormedCommRing = NonUnitalSeminormedCommRing.mk ⋯
A normed commutative ring is a non-unital normed commutative ring.
Equations
- NormedCommRing.toNonUnitalNormedCommRing = NonUnitalNormedCommRing.mk ⋯
A normed commutative ring is a seminormed commutative ring.
Equations
- NormedCommRing.toSeminormedCommRing = SeminormedCommRing.mk ⋯
Equations
A mixin class with the axiom ‖1‖ = 1
. Many NormedRing
s and all NormedField
s satisfy this
axiom.
The norm of the multiplicative identity is 1.
Instances
Equations
- NonUnitalSeminormedCommRing.toNonUnitalCommRing = NonUnitalCommRing.mk ⋯
Equations
- SeminormedCommRing.toCommRing = CommRing.mk ⋯
Equations
- NonUnitalNormedRing.toNormedAddCommGroup = NormedAddCommGroup.mk ⋯
Equations
- NonUnitalSeminormedRing.toSeminormedAddCommGroup = SeminormedAddCommGroup.mk ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
In a seminormed ring, the left-multiplication AddMonoidHom
is bounded.
In a seminormed ring, the right-multiplication AddMonoidHom
is bounded.
A non-unital subalgebra of a non-unital seminormed ring is also a non-unital seminormed ring, with the restriction of the norm.
Equations
- s.nonUnitalSeminormedRing = NonUnitalSeminormedRing.mk ⋯ ⋯
A non-unital subalgebra of a non-unital seminormed ring is also a non-unital seminormed ring, with the restriction of the norm.
A non-unital subalgebra of a non-unital normed ring is also a non-unital normed ring, with the restriction of the norm.
Equations
- s.nonUnitalNormedRing = NonUnitalNormedRing.mk ⋯ ⋯
A non-unital subalgebra of a non-unital normed ring is also a non-unital normed ring, with the restriction of the norm.
Equations
Equations
- ULift.nonUnitalSeminormedRing = NonUnitalSeminormedRing.mk ⋯ ⋯
Non-unital seminormed ring structure on the product of two non-unital seminormed rings, using the sup norm.
Equations
- Prod.nonUnitalSeminormedRing = NonUnitalSeminormedRing.mk ⋯ ⋯
Equations
- MulOpposite.instNonUnitalSeminormedRing = NonUnitalSeminormedRing.mk ⋯ ⋯
A subalgebra of a seminormed ring is also a seminormed ring, with the restriction of the norm.
Equations
- s.seminormedRing = SeminormedRing.mk ⋯ ⋯
A subalgebra of a seminormed ring is also a seminormed ring, with the restriction of the norm.
Equations
A subalgebra of a normed ring is also a normed ring, with the restriction of the norm.
Equations
- s.normedRing = NormedRing.mk ⋯ ⋯
A subalgebra of a normed ring is also a normed ring, with the restriction of the norm.
Equations
If α
is a seminormed ring, then ‖a ^ n‖₊ ≤ ‖a‖₊ ^ n
for n > 0
.
See also nnnorm_pow_le
.
If α
is a seminormed ring with ‖1‖₊ = 1
, then ‖a ^ n‖₊ ≤ ‖a‖₊ ^ n
.
See also nnnorm_pow_le'
.
If α
is a seminormed ring, then ‖a ^ n‖ ≤ ‖a‖ ^ n
for n > 0
. See also norm_pow_le
.
If α
is a seminormed ring with ‖1‖ = 1
, then ‖a ^ n‖ ≤ ‖a‖ ^ n
.
See also norm_pow_le'
.
Equations
- ULift.seminormedRing = SeminormedRing.mk ⋯ ⋯
Seminormed ring structure on the product of two seminormed rings, using the sup norm.
Equations
- Prod.seminormedRing = SeminormedRing.mk ⋯ ⋯
Equations
- MulOpposite.instSeminormedRing = SeminormedRing.mk ⋯ ⋯
A homomorphism f
between semi_normed_rings is bounded if there exists a positive
constant C
such that for all x
in α
, norm (f x) ≤ C * norm x
.
Instances For
Equations
- ULift.nonUnitalNormedRing = NonUnitalNormedRing.mk ⋯ ⋯
Non-unital normed ring structure on the product of two non-unital normed rings, using the sup norm.
Equations
- Prod.nonUnitalNormedRing = NonUnitalNormedRing.mk ⋯ ⋯
Equations
- MulOpposite.instNonUnitalNormedRing = NonUnitalNormedRing.mk ⋯ ⋯
Equations
- ULift.normedRing = NormedRing.mk ⋯ ⋯
Normed ring structure on the product of two normed rings, using the sup norm.
Equations
- Prod.normedRing = NormedRing.mk ⋯ ⋯
Equations
- MulOpposite.instNormedRing = NormedRing.mk ⋯ ⋯
Equations
- ULift.nonUnitalSeminormedCommRing = NonUnitalSeminormedCommRing.mk ⋯
Non-unital seminormed commutative ring structure on the product of two non-unital seminormed commutative rings, using the sup norm.
Equations
- Prod.nonUnitalSeminormedCommRing = NonUnitalSeminormedCommRing.mk ⋯
Equations
- MulOpposite.instNonUnitalSeminormedCommRing = NonUnitalSeminormedCommRing.mk ⋯
A non-unital subalgebra of a non-unital seminormed commutative ring is also a non-unital seminormed commutative ring, with the restriction of the norm.
Equations
- s.nonUnitalSeminormedCommRing = NonUnitalSeminormedCommRing.mk ⋯
A non-unital subalgebra of a non-unital normed commutative ring is also a non-unital normed commutative ring, with the restriction of the norm.
Equations
- s.nonUnitalNormedCommRing = NonUnitalNormedCommRing.mk ⋯
Equations
- ULift.nonUnitalNormedCommRing = NonUnitalNormedCommRing.mk ⋯
Non-unital normed commutative ring structure on the product of two non-unital normed commutative rings, using the sup norm.
Equations
- Prod.nonUnitalNormedCommRing = NonUnitalNormedCommRing.mk ⋯
Equations
- MulOpposite.instNonUnitalNormedCommRing = NonUnitalNormedCommRing.mk ⋯
Equations
- ULift.seminormedCommRing = SeminormedCommRing.mk ⋯
Seminormed commutative ring structure on the product of two seminormed commutative rings, using the sup norm.
Equations
- Prod.seminormedCommRing = SeminormedCommRing.mk ⋯
Equations
- MulOpposite.instSeminormedCommRing = SeminormedCommRing.mk ⋯
A subalgebra of a seminormed commutative ring is also a seminormed commutative ring, with the restriction of the norm.
Equations
- s.seminormedCommRing = SeminormedCommRing.mk ⋯
A subalgebra of a normed commutative ring is also a normed commutative ring, with the restriction of the norm.
Equations
- s.normedCommRing = NormedCommRing.mk ⋯
Equations
- ULift.normedCommRing = NormedCommRing.mk ⋯
Normed commutative ring structure on the product of two normed commutative rings, using the sup norm.
Equations
- Prod.normedCommRing = NormedCommRing.mk ⋯
Equations
- MulOpposite.instNormedCommRing = NormedCommRing.mk ⋯
The restriction of a power-multiplicative function to a subalgebra is power-multiplicative.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
norm
as a MonoidWithZeroHom
.
Instances For
nnnorm
as a MonoidWithZeroHom
.
Instances For
A normed field is a field with a norm satisfying ‖x y‖ = ‖x‖ ‖y‖.
- norm : α → ℝ
- add : α → α → α
- zero : α
- nsmul : ℕ → α → α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- mul : α → α → α
- one : α
- natCast : ℕ → α
- natCast_zero : NatCast.natCast 0 = 0
- natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
- npow : ℕ → α → α
- npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = Semiring.npow n x * x
- neg : α → α
- sub : α → α → α
- zsmul : ℤ → α → α
- zsmul_zero' : ∀ (a : α), Ring.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul (Int.ofNat n) a + a
- zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
- intCast : ℤ → α
- intCast_ofNat : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
- intCast_negSucc : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
- inv : α → α
- div : α → α → α
- zpow : ℤ → α → α
- zpow_zero' : ∀ (a : α), Field.zpow 0 a = 1
- zpow_succ' : ∀ (n : ℕ) (a : α), Field.zpow (Int.ofNat n.succ) a = Field.zpow (Int.ofNat n) a * a
- zpow_neg' : ∀ (n : ℕ) (a : α), Field.zpow (Int.negSucc n) a = (Field.zpow (↑n.succ) a)⁻¹
- exists_pair_ne : ∃ (x : α) (y : α), x ≠ y
- nnratCast : ℚ≥0 → α
- ratCast : ℚ → α
- nnqsmul : ℚ≥0 → α → α
- nnqsmul_def : ∀ (q : ℚ≥0) (a : α), Field.nnqsmul q a = ↑q * a
- qsmul : ℚ → α → α
- qsmul_def : ∀ (a : ℚ) (x : α), Field.qsmul a x = ↑a * x
- dist : α → α → ℝ
- edist : α → α → ENNReal
- edist_dist : ∀ (x y : α), PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
- toUniformSpace : UniformSpace α
- uniformity_dist : uniformity α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
- toBornology : Bornology α
The distance is induced by the norm.
The norm is multiplicative.
Instances
The distance is induced by the norm.
A nontrivially normed field is a normed field in which there is an element of norm different
from 0
and 1
. This makes it possible to bring any element arbitrarily close to 0
by
multiplication by the powers of any element, and thus to relate algebra and topology.
- norm : α → ℝ
- add : α → α → α
- zero : α
- nsmul : ℕ → α → α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- mul : α → α → α
- one : α
- natCast : ℕ → α
- natCast_zero : NatCast.natCast 0 = 0
- natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
- npow : ℕ → α → α
- npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = Semiring.npow n x * x
- neg : α → α
- sub : α → α → α
- zsmul : ℤ → α → α
- zsmul_zero' : ∀ (a : α), Ring.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul (Int.ofNat n) a + a
- zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
- intCast : ℤ → α
- intCast_ofNat : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
- intCast_negSucc : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
- inv : α → α
- div : α → α → α
- zpow : ℤ → α → α
- zpow_zero' : ∀ (a : α), Field.zpow 0 a = 1
- zpow_succ' : ∀ (n : ℕ) (a : α), Field.zpow (Int.ofNat n.succ) a = Field.zpow (Int.ofNat n) a * a
- zpow_neg' : ∀ (n : ℕ) (a : α), Field.zpow (Int.negSucc n) a = (Field.zpow (↑n.succ) a)⁻¹
- exists_pair_ne : ∃ (x : α) (y : α), x ≠ y
- nnratCast : ℚ≥0 → α
- ratCast : ℚ → α
- nnqsmul : ℚ≥0 → α → α
- nnqsmul_def : ∀ (q : ℚ≥0) (a : α), Field.nnqsmul q a = ↑q * a
- qsmul : ℚ → α → α
- qsmul_def : ∀ (a : ℚ) (x : α), Field.qsmul a x = ↑a * x
- dist : α → α → ℝ
- edist : α → α → ENNReal
- edist_dist : ∀ (x y : α), PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
- toUniformSpace : UniformSpace α
- uniformity_dist : uniformity α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
- toBornology : Bornology α
The norm attains a value exceeding 1.
Instances
The norm attains a value exceeding 1.
A densely normed field is a normed field for which the image of the norm is dense in ℝ≥0
,
which means it is also nontrivially normed. However, not all nontrivally normed fields are densely
normed; in particular, the Padic
s exhibit this fact.
- norm : α → ℝ
- add : α → α → α
- zero : α
- nsmul : ℕ → α → α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- mul : α → α → α
- one : α
- natCast : ℕ → α
- natCast_zero : NatCast.natCast 0 = 0
- natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
- npow : ℕ → α → α
- npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = Semiring.npow n x * x
- neg : α → α
- sub : α → α → α
- zsmul : ℤ → α → α
- zsmul_zero' : ∀ (a : α), Ring.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul (Int.ofNat n) a + a
- zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
- intCast : ℤ → α
- intCast_ofNat : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
- intCast_negSucc : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
- inv : α → α
- div : α → α → α
- zpow : ℤ → α → α
- zpow_zero' : ∀ (a : α), Field.zpow 0 a = 1
- zpow_succ' : ∀ (n : ℕ) (a : α), Field.zpow (Int.ofNat n.succ) a = Field.zpow (Int.ofNat n) a * a
- zpow_neg' : ∀ (n : ℕ) (a : α), Field.zpow (Int.negSucc n) a = (Field.zpow (↑n.succ) a)⁻¹
- exists_pair_ne : ∃ (x : α) (y : α), x ≠ y
- nnratCast : ℚ≥0 → α
- ratCast : ℚ → α
- nnqsmul : ℚ≥0 → α → α
- nnqsmul_def : ∀ (q : ℚ≥0) (a : α), Field.nnqsmul q a = ↑q * a
- qsmul : ℚ → α → α
- qsmul_def : ∀ (a : ℚ) (x : α), Field.qsmul a x = ↑a * x
- dist : α → α → ℝ
- edist : α → α → ENNReal
- edist_dist : ∀ (x y : α), PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
- toUniformSpace : UniformSpace α
- uniformity_dist : uniformity α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
- toBornology : Bornology α
The range of the norm is dense in the collection of nonnegative real numbers.
Instances
A densely normed field is always a nontrivially normed field. See note [lower instance priority].
Equations
- DenselyNormedField.toNontriviallyNormedField = NontriviallyNormedField.mk ⋯
Equations
- NormedField.toNormedDivisionRing = NormedDivisionRing.mk ⋯ ⋯
Equations
- NormedField.toNormedCommRing = NormedCommRing.mk ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
A normed field is nontrivially normed provided that the norm of some nonzero element is not one.
Instances For
Equations
Equations
A restatement of MetricSpace.tendsto_atTop
in terms of the norm.
A variant of NormedAddCommGroup.tendsto_atTop
that
uses ∃ N, ∀ n > N, ...
rather than ∃ N, ∀ n ≥ N, ...
This class states that a ring homomorphism is isometric. This is a sufficient assumption for a continuous semilinear map to be bounded and this is the main use for this typeclass.
The ring homomorphism is an isometry.
Instances
Equations
- ⋯ = ⋯
Induced normed structures #
A non-unital ring homomorphism from a NonUnitalRing
to a NonUnitalSeminormedRing
induces a NonUnitalSeminormedRing
structure on the domain.
See note [reducible non-instances]
Equations
Instances For
An injective non-unital ring homomorphism from a NonUnitalRing
to a
NonUnitalNormedRing
induces a NonUnitalNormedRing
structure on the domain.
See note [reducible non-instances]
Equations
- NonUnitalNormedRing.induced R S f hf = NonUnitalNormedRing.mk ⋯ ⋯
Instances For
A non-unital ring homomorphism from a Ring
to a SeminormedRing
induces a
SeminormedRing
structure on the domain.
See note [reducible non-instances]
Equations
- SeminormedRing.induced R S f = SeminormedRing.mk ⋯ ⋯
Instances For
An injective non-unital ring homomorphism from a Ring
to a NormedRing
induces a
NormedRing
structure on the domain.
See note [reducible non-instances]
Equations
- NormedRing.induced R S f hf = NormedRing.mk ⋯ ⋯
Instances For
A non-unital ring homomorphism from a NonUnitalCommRing
to a NonUnitalSeminormedCommRing
induces a NonUnitalSeminormedCommRing
structure on the domain.
See note [reducible non-instances]
Equations
Instances For
An injective non-unital ring homomorphism from a NonUnitalCommRing
to a
NonUnitalNormedCommRing
induces a NonUnitalNormedCommRing
structure on the domain.
See note [reducible non-instances]
Equations
Instances For
A non-unital ring homomorphism from a CommRing
to a SeminormedRing
induces a
SeminormedCommRing
structure on the domain.
See note [reducible non-instances]
Equations
Instances For
An injective non-unital ring homomorphism from a CommRing
to a NormedRing
induces a
NormedCommRing
structure on the domain.
See note [reducible non-instances]
Equations
- NormedCommRing.induced R S f hf = NormedCommRing.mk ⋯
Instances For
An injective non-unital ring homomorphism from a DivisionRing
to a NormedRing
induces a
NormedDivisionRing
structure on the domain.
See note [reducible non-instances]
Equations
- NormedDivisionRing.induced R S f hf = NormedDivisionRing.mk ⋯ ⋯
Instances For
An injective non-unital ring homomorphism from a Field
to a NormedRing
induces a
NormedField
structure on the domain.
See note [reducible non-instances]
Equations
- NormedField.induced R S f hf = NormedField.mk ⋯ ⋯
Instances For
A ring homomorphism from a Ring R
to a SeminormedRing S
which induces the norm structure
SeminormedRing.induced
makes R
satisfy ‖(1 : R)‖ = 1
whenever ‖(1 : S)‖ = 1
.
Equations
Equations
- SubringClass.toNormedRing s = NormedRing.induced (↥s) R (SubringClass.subtype s) ⋯