Commit 2025-08-13 19:34 4ce895f5

View on Github →

feat: orderOf x ≠ 0 ↔ IsOfFinOrder x (#28147) Also make the two existing lemmas simp. From ClassFieldTheory

Estimated changes

Modified Mathlib/Data/Rat/Lemmas.lean

Modified Mathlib/Data/Real/Irrational.lean

added theorem Irrational.ne_rational

modified theorem irrational_iff_ne_rational

Modified Mathlib/GroupTheory/OrderOfElement.lean

added theorem orderOf_ne_zero_iff

Modified Mathlib/NumberTheory/DiophantineApproximation/Basic.lean

Modified Mathlib/NumberTheory/Transcendental/Liouville/Basic.lean

Modified Mathlib/Topology/Instances/AddCircle/Defs.lean

added theorem AddCircle.isOfFinAddOrder_iff_exists_rat_eq_div

added theorem AddCircle.not_isOfFinAddOrder_iff_forall_rat_ne_div

Modified Mathlib/Topology/Instances/AddCircle/DenseSubgroup.lean