Theorems · Definition · group theory
MulEquiv.prodUnits
{M : Type u_3} → {N : Type u_4} → [inst : Monoid M] → [inst_1 : Monoid N] → (M × N)ˣ ≃* Mˣ × NˣThe monoid equivalence between units of a product of two monoids, and the product of the units of each monoid.
- Defined in
- Mathlib.Algebra.Group.Prod
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 27 from the axioms · uses propext, 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
- Monoidstatement and proof · cited by 3,887
- Unitsstatement and proof · cited by 2,804
- Units.valproof · cited by 1,966
- MulEquivstatement · cited by 1,142
- Units.mapproof · cited by 95
- MonoidHom.sndproof · cited by 31
- MonoidHom.fstproof · cited by 28
- MonoidHom.prodproof · cited by 15
Cited by8
Results whose statement or proof uses this declaration.
- Nat.totient_mulproof · cited by 5
- ArithmeticFunction.carmichael_lcmproof · cited by 2
- ZMod.not_isCyclic_units_of_mul_coprimeproof · cited by 1
- Prod.isUnit_iffproof · cited by 1
- ZMod.isCyclic_units_four_mul_iffproof · cited by 1
- ZMod.isCyclic_units_two_mul_iff_of_oddproof · cited by 1
- Homeomorph.prodUnitsproof · cited by 0
- Prod.associated_iffproof · cited by 0