Theorem ofNat_eq_one

Modification history

2025-01-06 19:13
Mathlib/Algebra/Order/Kleene.lean
feat(RingTheory/Ideal): 37 cast to an ideal is just the whole ring. (#20244) …
Added ofNat_eq_oneView on Github →