Theorem Real.norm_natCast

Modification history

2026-02-09 11:06
Mathlib/Analysis/Normed/Group/Basic.lean
refactor(Analysis/Normed/Group): split large file (#34802) …
Modified Real.norm_natCastView on Github →
2025-09-08 19:22
Mathlib/Analysis/Normed/Group/Basic.lean
feat(NumberTheory/Divisors): divisors antidiagonal tsum (#28690)
Modified Real.norm_natCastView on Github →
2024-08-29 12:34
Mathlib/Analysis/Normed/Group/Basic.lean
feat(RCLike): `nnnorm` lemmas (#16144) …
Modified Real.norm_natCastView on Github →
2024-04-07 17:47
Mathlib/Analysis/Normed/Group/Basic.lean
chore: Rename `coe_nat`/`coe_int`/`coe_rat` to `natCast`/`intCast`/`ratCast` (#11499) …
Added Real.norm_natCastView on Github →