Theorem one_eq_of_le_of_one_eq

Modification history

2026-11-10 16:49
Mathlib/Algebra/Order/IsBotOne.lean
feat: `@[gcongr]` for `eq_top_mono` and friends (#44334) …
Added one_eq_of_le_of_one_eqView on Github →