Theorems · Theorem · group theory
Ring.inverse_non_unit
∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] (x : M₀), ¬IsUnit x → Ring.inverse x = 0By definition, if x is not invertible then inverse x = 0.
- Cited by
- 26 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- MonoidWithZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- IsUnitstatement and proof · cited by 1,602
- MonoidWithZerostatement and proof · cited by 456
- Ring.inversestatement · cited by 160
Cited by26
Results whose statement or proof uses this declaration.
- Matrix.nonsing_inv_apply_not_isUnitproof · cited by 7
- Matrix.nonsing_inv_eq_ringInverseproof · cited by 7
- Matrix.det_nonsing_invproof · cited by 4
- Ring.inverse_eq_invproof · cited by 4
- isUnit_ringInverseproof · cited by 2
- ContinuousLinearMap.inverse_eq_ringInverseproof · cited by 2
- Ring.mul_inverse_rev'proof · cited by 2
- MulChar.inv_applyproof · cited by 2
- Ring.inverse_starproof · cited by 2
- spectrum.resolvent_zero_of_mem_spectrumproof · cited by 2
- Ring.inverse_zeroproof · cited by 2
- spectrum.units_smul_resolventproof · cited by 1