Theorems · Definition · group theory
MulHom.unop
{M : Type u_3} → {N : Type u_4} → [inst : Mul M] → [inst_1 : Mul N] → (Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ) ≃ (M →ₙ* N)The 'unopposite' of a semigroup homomorphism Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ. Inverse to MulHom.op.
- Defined in
- Mathlib.Algebra.Group.Equiv.Opposite
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 19 from the axioms · uses Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Equivstatement · cited by 8,337
- Equiv.symmproof · cited by 3,681
- MulOppositestatement · cited by 1,135
- MulHomstatement · cited by 299
- MulHom.opproof · cited by 2
Cited by1
Results whose statement or proof uses this declaration.
- NonUnitalRingHom.opproof · cited by 2