Theorems · Definition · group theory
Units.embedProduct
(α : Type u_6) → [inst : Monoid α] → αˣ →* α × αᵐᵒᵖ
Canonical homomorphism of monoids from αˣ into α × αᵐᵒᵖ.
Used mainly to define the natural topology of αˣ.
- Defined in
- Mathlib.Algebra.Group.Prod
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 23 from the axioms · uses propext, Quot.sound
- Assumes
- Monoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Monoidstatement and proof · cited by 3,887
- MonoidHomstatement · cited by 3,629
- Unitsstatement and proof · cited by 2,804
- Units.valproof · cited by 1,966
- MulOppositestatement · cited by 1,135
- MulOpposite.opproof · cited by 520
Cited by12
Results whose statement or proof uses this declaration.
- Units.isInducing_embedProductstatement · cited by 4
- Units.continuous_embedProductstatement · cited by 3
- Units.isEmbedding_embedProductstatement · cited by 3
- Units.embedProduct_applystatement and proof · cited by 3
- Units.isClosedEmbedding_embedProductstatement and proof · cited by 2
- Units.topology_eq_infproof · cited by 1
- Units.range_embedProductstatement and proof · cited by 1
- Units.embedProduct_injectivestatement and proof · cited by 1
- IsOpenUnits.of_isAdicproof · cited by 0
- Units.embed_product_starstatement · cited by 0
- Matrix.GeneralLinearGroup.continuous_upperRightHomproof · cited by 0
- Units.isOpenMap_mapproof · cited by 0