Normed fields #
In this file we define (semi)normed rings and fields. We also prove some theorems about these definitions.
- norm : α → ℝ
- add : α → α → α
- zero : α
- nsmul : ℕ → α → α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x
- neg : α → α
- sub : α → α → α
- zsmul : ℤ → α → α
- zsmul_zero' : ∀ (a : α), SubNegMonoid.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (Int.ofNat (Nat.succ n)) a = a + SubNegMonoid.zsmul (Int.ofNat n) a
- zsmul_neg' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑(Nat.succ n)) 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.fst p.snd < ε}
- toBornology : Bornology α
The distance is induced by the norm.
The norm is submultiplicative.
A non-unital seminormed ring is a not-necessarily-unital ring
endowed with a seminorm which satisfies the inequality ‖x y‖ ≤ ‖x‖ ‖y‖
.
Instances
- norm : α → ℝ
- add : α → α → α
- zero : α
- nsmul : ℕ → α → α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n 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 = x * Semiring.npow n x
- neg : α → α
- sub : α → α → α
- zsmul : ℤ → α → α
- zsmul_zero' : ∀ (a : α), Ring.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.ofNat (Nat.succ n)) a = a + Ring.zsmul (Int.ofNat n) a
- zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑(Nat.succ n)) 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.fst p.snd < ε}
- toBornology : Bornology α
The distance is induced by the norm.
The norm is submultiplicative.
A seminormed ring is a ring endowed with a seminorm which satisfies the inequality
‖x y‖ ≤ ‖x‖ ‖y‖
.
Instances
A seminormed ring is a non-unital seminormed ring.
- norm : α → ℝ
- add : α → α → α
- zero : α
- nsmul : ℕ → α → α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x
- neg : α → α
- sub : α → α → α
- zsmul : ℤ → α → α
- zsmul_zero' : ∀ (a : α), SubNegMonoid.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (Int.ofNat (Nat.succ n)) a = a + SubNegMonoid.zsmul (Int.ofNat n) a
- zsmul_neg' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑(Nat.succ n)) 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.fst p.snd < ε}
- toBornology : Bornology α
The distance is induced by the norm.
The norm is submultiplicative.
A non-unital normed ring is a not-necessarily-unital ring
endowed with a norm which satisfies the inequality ‖x y‖ ≤ ‖x‖ ‖y‖
.
Instances
A non-unital normed ring is a non-unital seminormed ring.
- norm : α → ℝ
- add : α → α → α
- zero : α
- nsmul : ℕ → α → α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n 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 = x * Semiring.npow n x
- neg : α → α
- sub : α → α → α
- zsmul : ℤ → α → α
- zsmul_zero' : ∀ (a : α), Ring.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.ofNat (Nat.succ n)) a = a + Ring.zsmul (Int.ofNat n) a
- zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑(Nat.succ n)) 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.fst p.snd < ε}
- toBornology : Bornology α
The distance is induced by the norm.
The norm is submultiplicative.
A normed ring is a ring endowed with a norm which satisfies the inequality ‖x y‖ ≤ ‖x‖ ‖y‖
.
Instances
- norm : α → ℝ
- add : α → α → α
- zero : α
- nsmul : ℕ → α → α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n 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 = x * Semiring.npow n x
- neg : α → α
- sub : α → α → α
- zsmul : ℤ → α → α
- zsmul_zero' : ∀ (a : α), Ring.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.ofNat (Nat.succ n)) a = a + Ring.zsmul (Int.ofNat n) a
- zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑(Nat.succ n)) 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 (Nat.succ n)) a = a * DivisionRing.zpow (Int.ofNat n) a
- zpow_neg' : ∀ (n : ℕ) (a : α), DivisionRing.zpow (Int.negSucc n) a = (DivisionRing.zpow (↑(Nat.succ n)) a)⁻¹
- exists_pair_ne : ∃ x y, x ≠ y
- ratCast : ℚ → α
- ratCast_mk : ∀ (a : ℤ) (b : ℕ) (h1 : b ≠ 0) (h2 : Nat.Coprime (Int.natAbs a) b), ↑(Rat.mk' a b) = ↑a * (↑b)⁻¹
- qsmul : ℚ → α → α
- qsmul_eq_mul' : ∀ (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.fst p.snd < ε}
- toBornology : Bornology α
The distance is induced by the norm.
The norm is multiplicative.
A normed division ring is a division ring endowed with a seminorm which satisfies the equality
‖x y‖ = ‖x‖ ‖y‖
.
Instances
A normed division ring is a normed ring.
A normed ring is a seminormed ring.
A normed ring is a non-unital normed ring.
- norm : α → ℝ
- add : α → α → α
- zero : α
- nsmul : ℕ → α → α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n 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 = x * Semiring.npow n x
- neg : α → α
- sub : α → α → α
- zsmul : ℤ → α → α
- zsmul_zero' : ∀ (a : α), Ring.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.ofNat (Nat.succ n)) a = a + Ring.zsmul (Int.ofNat n) a
- zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑(Nat.succ n)) 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.fst p.snd < ε}
- toBornology : Bornology α
Multiplication is commutative.
A seminormed commutative ring is a commutative ring endowed with a seminorm which satisfies
the inequality ‖x y‖ ≤ ‖x‖ ‖y‖
.
Instances
- norm : α → ℝ
- add : α → α → α
- zero : α
- nsmul : ℕ → α → α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n 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 = x * Semiring.npow n x
- neg : α → α
- sub : α → α → α
- zsmul : ℤ → α → α
- zsmul_zero' : ∀ (a : α), Ring.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.ofNat (Nat.succ n)) a = a + Ring.zsmul (Int.ofNat n) a
- zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑(Nat.succ n)) 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.fst p.snd < ε}
- toBornology : Bornology α
Multiplication is commutative.
A normed commutative ring is a commutative ring endowed with a norm which satisfies
the inequality ‖x y‖ ≤ ‖x‖ ‖y‖
.
Instances
A normed commutative ring is a seminormed commutative ring.
The norm of the multiplicative identity is 1.
A mixin class with the axiom ‖1‖ = 1
. Many NormedRing
s and all NormedField
s satisfy this
axiom.
Instances
In a seminormed ring, the left-multiplication AddMonoidHom
is bounded.
In a seminormed ring, the right-multiplication AddMonoidHom
is bounded.
Non-unital seminormed ring structure on the product of two non-unital seminormed rings, using the sup norm.
Non-unital seminormed ring structure on the product of finitely many non-unital seminormed rings, using the sup norm.
A subalgebra of a seminormed ring is also a seminormed ring, with the restriction of the norm.
See note [implicit instance arguments].
A subalgebra of a normed ring is also a normed ring, with the restriction of the norm.
See note [implicit instance arguments].
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'
.
Seminormed ring structure on the product of two seminormed rings, using the sup norm.
Seminormed ring structure on the product of finitely many seminormed rings, using the sup norm.
Non-unital normed ring structure on the product of two non-unital normed rings, using the sup norm.
Normed ring structure on the product of finitely many non-unital normed rings, using the sup norm.
Normed ring structure on the product of two normed rings, using the sup norm.
Normed ring structure on the product of finitely many normed rings, using the sup norm.
A seminormed ring is a topological ring.
norm
as a MonoidWithZeroHom
.
Instances For
nnnorm
as a MonoidWithZeroHom
.
Instances For
Multiplication on the left by a nonzero element of a normed division ring tends to infinity at
infinity. TODO: use Bornology.cobounded
instead of Filter.comap Norm.norm Filter.atTop
.
Multiplication on the right by a nonzero element of a normed division ring tends to infinity at
infinity. TODO: use Bornology.cobounded
instead of Filter.comap Norm.norm Filter.atTop
.
A normed division ring is a topological division ring.
- norm : α → ℝ
- add : α → α → α
- zero : α
- nsmul : ℕ → α → α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n 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 = x * Semiring.npow n x
- neg : α → α
- sub : α → α → α
- zsmul : ℤ → α → α
- zsmul_zero' : ∀ (a : α), Ring.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.ofNat (Nat.succ n)) a = a + Ring.zsmul (Int.ofNat n) a
- zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑(Nat.succ n)) 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 (Nat.succ n)) a = a * Field.zpow (Int.ofNat n) a
- zpow_neg' : ∀ (n : ℕ) (a : α), Field.zpow (Int.negSucc n) a = (Field.zpow (↑(Nat.succ n)) a)⁻¹
- exists_pair_ne : ∃ x y, x ≠ y
- ratCast : ℚ → α
- ratCast_mk : ∀ (a : ℤ) (b : ℕ) (h1 : b ≠ 0) (h2 : Nat.Coprime (Int.natAbs a) b), ↑(Rat.mk' a b) = ↑a * (↑b)⁻¹
- qsmul : ℚ → α → α
- qsmul_eq_mul' : ∀ (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.fst p.snd < ε}
- toBornology : Bornology α
The distance is induced by the norm.
The norm is multiplicative.
A normed field is a field with a norm satisfying ‖x y‖ = ‖x‖ ‖y‖.
Instances
- norm : α → ℝ
- add : α → α → α
- zero : α
- nsmul : ℕ → α → α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n 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 = x * Semiring.npow n x
- neg : α → α
- sub : α → α → α
- zsmul : ℤ → α → α
- zsmul_zero' : ∀ (a : α), Ring.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.ofNat (Nat.succ n)) a = a + Ring.zsmul (Int.ofNat n) a
- zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑(Nat.succ n)) 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 (Nat.succ n)) a = a * Field.zpow (Int.ofNat n) a
- zpow_neg' : ∀ (n : ℕ) (a : α), Field.zpow (Int.negSucc n) a = (Field.zpow (↑(Nat.succ n)) a)⁻¹
- exists_pair_ne : ∃ x y, x ≠ y
- ratCast : ℚ → α
- ratCast_mk : ∀ (a : ℤ) (b : ℕ) (h1 : b ≠ 0) (h2 : Nat.Coprime (Int.natAbs a) b), ↑(Rat.mk' a b) = ↑a * (↑b)⁻¹
- qsmul : ℚ → α → α
- qsmul_eq_mul' : ∀ (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.fst p.snd < ε}
- toBornology : Bornology α
The norm attains a value exceeding 1.
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.
Instances
- norm : α → ℝ
- add : α → α → α
- zero : α
- nsmul : ℕ → α → α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n 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 = x * Semiring.npow n x
- neg : α → α
- sub : α → α → α
- zsmul : ℤ → α → α
- zsmul_zero' : ∀ (a : α), Ring.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.ofNat (Nat.succ n)) a = a + Ring.zsmul (Int.ofNat n) a
- zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑(Nat.succ n)) 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 (Nat.succ n)) a = a * Field.zpow (Int.ofNat n) a
- zpow_neg' : ∀ (n : ℕ) (a : α), Field.zpow (Int.negSucc n) a = (Field.zpow (↑(Nat.succ n)) a)⁻¹
- exists_pair_ne : ∃ x y, x ≠ y
- ratCast : ℚ → α
- ratCast_mk : ∀ (a : ℤ) (b : ℕ) (h1 : b ≠ 0) (h2 : Nat.Coprime (Int.natAbs a) b), ↑(Rat.mk' a b) = ↑a * (↑b)⁻¹
- qsmul : ℚ → α → α
- qsmul_eq_mul' : ∀ (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.fst p.snd < ε}
- toBornology : Bornology α
The range of the norm is dense in the collection of nonnegative real numbers.
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.
Instances
A densely normed field is always a nontrivially normed field. See note [lower instance priority].
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, ...
The ring homomorphism is an isometry.
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.
Instances
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]
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]
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]
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]
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]
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]
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]
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]
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
.