Theorems · Definition · group theory
MulEquiv.withZero
{α : Type u_1} → {β : Type u_2} → [inst : Group α] → [inst_1 : Group β] → α ≃* β ≃ (WithZero α ≃* WithZero β)A version of Equiv.optionCongr for WithZero.
- Defined in
- Mathlib.Algebra.GroupWithZero.WithZero
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 25 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Equivstatement · cited by 8,337
- Groupstatement and proof · cited by 6,238
- MulEquivstatement and proof · cited by 1,142
- WithZerostatement and proof · cited by 586
- MulEquiv.symmproof · cited by 482
- MonoidHomClass.toMonoidHomproof · cited by 294
- WithZero.map'proof · cited by 45
- WithZero.unzeroproof · cited by 38
Cited by9
Results whose statement or proof uses this declaration.
- Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulIntproof · cited by 11
- OrderMonoidIso.withZeroproof · cited by 6
- LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrderedproof · cited by 4
- MulEquiv.withZero_symm_apply_applystatement and proof · cited by 1
- MulEquiv.unzeroproof · cited by 0
- MulEquiv.withZero_apply_applystatement and proof · cited by 0
- MulEquiv.withZero_apply_symm_applystatement and proof · cited by 0
- MulEquiv.withZero_symm_apply_symm_applystatement and proof · cited by 0