Theorems · Definition · commutative algebra
IsLeftRegular
{R : Type u_1} → [Mul R] → R → PropA left-regular element is an element c such that multiplication on the left by c
is injective.
- Defined in
- Mathlib.Algebra.Regular.Defs
- Cited by
- 97 results in Mathlib
- Foundations
- Depth 4 from the axioms, rests on 9 definitions · uses no axioms
- Assumes
- Mul
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by103
Results whose statement or proof uses this declaration.
- IsRegular.leftstatement · cited by 39
- isRegular_iffstatement and proof · cited by 6
- IsLeftRegular.mulstatement and proof · cited by 5
- IsLeftRegular.of_mulstatement and proof · cited by 5
- IsLeftRegular.powstatement and proof · cited by 5
- Commute.isRegular_iffstatement and proof · cited by 5
- IsLeftCancelMulZero.mul_left_cancel_of_ne_zerostatement · cited by 4
- IsLeftRegular.allstatement · cited by 4
- IsLeftRegular.pow_injectivestatement and proof · cited by 4
- IsLeftRegular.right_of_commutestatement and proof · cited by 4
- IsLeftRegular.mul_left_eq_zero_iffstatement and proof · cited by 3
- IsLeftRegular.starstatement and proof · cited by 3