Theorems · Definition · group theory
Submonoid.opEquiv
{M : Type u_2} → [inst : MulOneClass M] → Submonoid M ≃o Submonoid MᵐᵒᵖA submonoid H of M determines a submonoid H.op of the opposite monoid Mᵐᵒᵖ.
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 25 from the axioms · uses propext, Quot.sound
- Assumes
- MulOneClass
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.
- Submonoidstatement and proof · cited by 3,086
- MulOppositestatement · cited by 1,135
- MulOneClassstatement and proof · cited by 1,018
- OrderIsostatement · cited by 874
- Submonoid.opproof · cited by 38
- Submonoid.unopproof · cited by 26
- Submonoid.op_unopproof · cited by 1
- Submonoid.op_le_op_iffproof · cited by 0
- Submonoid.unop_opproof · cited by 0
Cited by18
Results whose statement or proof uses this declaration.
- Submonoid.op_injectiveproof · cited by 2
- Submonoid.unop_injectiveproof · cited by 2
- Submonoid.op_botproof · cited by 1
- Submonoid.op_injproof · cited by 1
- Submonoid.op_sInfproof · cited by 1
- Submonoid.unop_botproof · cited by 1
- Submonoid.opEquiv_applystatement and proof · cited by 0
- Submonoid.opEquiv_symm_applystatement and proof · cited by 0
- Submonoid.op_iInfproof · cited by 0
- Submonoid.op_iSupproof · cited by 0
- Submonoid.op_sSupproof · cited by 0
- Submonoid.op_supproof · cited by 0