Theorem real.norm_two
Modification history
2022-12-04 17:00
src/analysis/normed/group/basic.lean
feat(algebra/order/zero_le_one): generalize lemmas (#17465) …
Modified real.norm_twoView on Github →2022-11-17 13:13
src/analysis/normed/group/basic.lean
refactor(analysis): change the symbol for norm to align with the unicode spec (#17575) …
Modified real.norm_twoView on Github →2022-10-29 09:38
src/analysis/normed/field/basic.lean
chore(analysis/normed/group/basic): Earlier `ℝ` lemmas (#16972) …
Modified real.norm_twoView on Github →2022-03-02 21:08
src/analysis/normed/normed_field.lean
refactor(analysis/normed_space/basic): split into normed_space and ../normed/normed_field (#12410) …
Modified real.norm_twoView on Github →2021-06-23 17:29
src/analysis/normed_space/basic.lean
feat(analysis/normed_space/basic): add has_nnnorm (#7986) …
Modified real.norm_twoView on Github →2020-10-19 11:39
src/analysis/normed_space/basic.lean
feat(algebra/ordered_semiring): relax 0 < 1 to 0 ≤ 1 (#4363) …
Modified real.norm_twoView on Github →2020-09-28 11:21
src/analysis/normed_space/basic.lean
chore(algebra/ordered_ring): remove duplicate lemma (#4295) …
Modified real.norm_twoView on Github →