Theorem exists_right_inv_of_exists_left_inv

Modification history

2025-02-04 15:13

Mathlib/Algebra/GroupWithZero/Basic.lean

refactor: introduce `Ideal.IsTwoSided` class for quotients of noncommutative rings (#17930)

Added exists_right_inv_of_exists_left_inv View on Github →