Commit 2025-01-29 23:20 789550e9
View on Github →feat(NumberTheory/NumberField/FinitePlaces): change one lemma (#21187)
lemma one_lt_norm: 1 < (absNorm v.asIdeal : NNReal)
becomes
lemma one_lt_norm_nnreal : 1 < (absNorm v.asIdeal : NNReal)
and we add
lemma one_lt_norm : 1 < absNorm v.asIdeal