Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_unit.exists_left_inv

Modification history

2021-06-10 01:51
src/algebra/group/units.lean
feat(ring_theory/ideal): generalize to noncommutative rings (#7654) …
Added is_unit.exists_left_invView on Github →