ProdHom

📁 Source: Mathlib/Algebra/GroupWithZero/ProdHom.lean

Statistics

Metric	Count
Definitions fst, inl, inr, snd	4
Theorems commute_inl_inr, fst_apply_coe, fst_comp_inl, fst_comp_inr, fst_inl, fst_inr_apply_of_ne_zero, fst_surjective, inl_apply_unit, inl_injective, inl_mul_inr_eq_mk_of_unit, inr_apply_unit, inr_injective, one_apply_apply_eq, one_comp, snd_apply_coe, snd_comp_inl, snd_comp_inr, snd_inl_apply_of_ne_zero, snd_inr, snd_surjective	20
Total	24

MonoidWithZeroHom

Definitions

Name	Category	Theorems
fst 📖	CompOp	8 math math: fst_mono, fst_comp_inl, fst_apply_coe, fst_inl, fst_surjective, LinearOrderedCommGroupWithZero.fst_apply, fst_inr_apply_of_ne_zero, fst_comp_inr
inl 📖	CompOp	11 math math: snd_comp_inl, inl_strictMono, fst_comp_inl, inl_mul_inr_eq_mk_of_unit, snd_inl_apply_of_ne_zero, inl_injective, fst_inl, inl_mono, LinearOrderedCommGroupWithZero.inl_apply, commute_inl_inr, inl_apply_unit
inr 📖	CompOp	11 math math: inl_mul_inr_eq_mk_of_unit, inr_mono, snd_inr, snd_comp_inr, inr_apply_unit, fst_inr_apply_of_ne_zero, inr_strictMono, LinearOrderedCommGroupWithZero.inr_apply, inr_injective, commute_inl_inr, fst_comp_inr
snd 📖	CompOp	7 math math: snd_comp_inl, snd_inr, snd_inl_apply_of_ne_zero, snd_mono, snd_comp_inr, snd_apply_coe, snd_surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commute_inl_inr 📖	mathematical	—	Commute WithZero Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulZeroClass.toMul WithZero.instMulZeroClass Prod.instMul Units.instMul DFunLike.coe MonoidWithZeroHom MonoidWithZero.toMulZeroOneClass WithZero.instMulZeroOneClass Prod.instMulOneClass Units.instMulOneClass funLike inl inr	—	GroupWithZero.eq_zero_or_unit map_zero MonoidWithZeroHomClass.toZeroHomClass monoidWithZeroHomClass GroupWithZero.toNontrivial MulZeroClass.zero_mul MulZeroClass.mul_zero mul_one one_mul
fst_apply_coe 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom WithZero Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero WithZero.instMulZeroOneClass Prod.instMulOneClass Units.instMulOneClass MonoidWithZero.toMulZeroOneClass funLike fst WithZero.coe Units.val	—	—
fst_comp_inl 📖	mathematical	—	comp WithZero Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MonoidWithZero.toMulZeroOneClass WithZero.instMulZeroOneClass Prod.instMulOneClass Units.instMulOneClass fst inl id	—	ext fst_inl
fst_comp_inr 📖	mathematical	—	comp WithZero Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MonoidWithZero.toMulZeroOneClass WithZero.instMulZeroOneClass Prod.instMulOneClass Units.instMulOneClass fst inr MonoidWithZeroHom one GroupWithZero.toNontrivial GroupWithZero.noZeroDivisors	—	ext GroupWithZero.toNontrivial GroupWithZero.noZeroDivisors GroupWithZero.eq_zero_or_unit map_zero MonoidWithZeroHomClass.toZeroHomClass monoidWithZeroHomClass one_apply_zero one_apply_val_unit
fst_inl 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom WithZero Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero WithZero.instMulZeroOneClass Prod.instMulOneClass Units.instMulOneClass MonoidWithZero.toMulZeroOneClass funLike fst inl	—	GroupWithZero.eq_zero_or_unit map_zero MonoidWithZeroHomClass.toZeroHomClass monoidWithZeroHomClass GroupWithZero.toNontrivial
fst_inr_apply_of_ne_zero 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom WithZero Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero WithZero.instMulZeroOneClass Prod.instMulOneClass Units.instMulOneClass MonoidWithZero.toMulZeroOneClass funLike fst inr InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	comp_apply GroupWithZero.toNontrivial GroupWithZero.noZeroDivisors fst_comp_inr one_apply_of_ne_zero
fst_surjective 📖	mathematical	—	WithZero Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero DFunLike.coe MonoidWithZeroHom WithZero.instMulZeroOneClass Prod.instMulOneClass Units.instMulOneClass MonoidWithZero.toMulZeroOneClass funLike fst	—	fst_inl
inl_apply_unit 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom WithZero Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MonoidWithZero.toMulZeroOneClass WithZero.instMulZeroOneClass Prod.instMulOneClass Units.instMulOneClass funLike inl Units.val WithZero.coe Units.instOne	—	GroupWithZero.toNontrivial
inl_injective 📖	mathematical	—	WithZero Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero DFunLike.coe MonoidWithZeroHom MonoidWithZero.toMulZeroOneClass WithZero.instMulZeroOneClass Prod.instMulOneClass Units.instMulOneClass funLike inl	—	fst_inl
inl_mul_inr_eq_mk_of_unit 📖	mathematical	—	WithZero Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulZeroClass.toMul WithZero.instMulZeroClass Prod.instMul Units.instMul DFunLike.coe MonoidWithZeroHom MonoidWithZero.toMulZeroOneClass WithZero.instMulZeroOneClass Prod.instMulOneClass Units.instMulOneClass funLike inl Units.val inr WithZero.coe	—	GroupWithZero.toNontrivial mul_one one_mul
inr_apply_unit 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom WithZero Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MonoidWithZero.toMulZeroOneClass WithZero.instMulZeroOneClass Prod.instMulOneClass Units.instMulOneClass funLike inr Units.val WithZero.coe Units.instOne	—	GroupWithZero.toNontrivial
inr_injective 📖	mathematical	—	WithZero Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero DFunLike.coe MonoidWithZeroHom MonoidWithZero.toMulZeroOneClass WithZero.instMulZeroOneClass Prod.instMulOneClass Units.instMulOneClass funLike inr	—	snd_inr
one_apply_apply_eq 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom funLike one MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero GroupWithZero.toNontrivial GroupWithZero.noZeroDivisors	—	GroupWithZero.toNontrivial GroupWithZero.noZeroDivisors eq_or_ne map_zero MonoidWithZeroHomClass.toZeroHomClass monoidWithZeroHomClass one_apply_zero one_apply_of_ne_zero map_ne_zero
one_comp 📖	mathematical	—	comp MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero MonoidWithZeroHom one GroupWithZero.toNontrivial GroupWithZero.noZeroDivisors	—	ext GroupWithZero.toNontrivial GroupWithZero.noZeroDivisors one_apply_apply_eq
snd_apply_coe 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom WithZero Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero WithZero.instMulZeroOneClass Prod.instMulOneClass Units.instMulOneClass MonoidWithZero.toMulZeroOneClass funLike snd WithZero.coe Units.val	—	—
snd_comp_inl 📖	mathematical	—	comp WithZero Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MonoidWithZero.toMulZeroOneClass WithZero.instMulZeroOneClass Prod.instMulOneClass Units.instMulOneClass snd inl MonoidWithZeroHom one GroupWithZero.toNontrivial GroupWithZero.noZeroDivisors	—	ext GroupWithZero.toNontrivial GroupWithZero.noZeroDivisors GroupWithZero.eq_zero_or_unit map_zero MonoidWithZeroHomClass.toZeroHomClass monoidWithZeroHomClass one_apply_zero one_apply_val_unit
snd_comp_inr 📖	mathematical	—	comp WithZero Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MonoidWithZero.toMulZeroOneClass WithZero.instMulZeroOneClass Prod.instMulOneClass Units.instMulOneClass snd inr id	—	ext snd_inr
snd_inl_apply_of_ne_zero 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom WithZero Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero WithZero.instMulZeroOneClass Prod.instMulOneClass Units.instMulOneClass MonoidWithZero.toMulZeroOneClass funLike snd inl InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	comp_apply GroupWithZero.toNontrivial GroupWithZero.noZeroDivisors snd_comp_inl one_apply_of_ne_zero
snd_inr 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom WithZero Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero WithZero.instMulZeroOneClass Prod.instMulOneClass Units.instMulOneClass MonoidWithZero.toMulZeroOneClass funLike snd inr	—	GroupWithZero.eq_zero_or_unit map_zero MonoidWithZeroHomClass.toZeroHomClass monoidWithZeroHomClass GroupWithZero.toNontrivial
snd_surjective 📖	mathematical	—	WithZero Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero DFunLike.coe MonoidWithZeroHom WithZero.instMulZeroOneClass Prod.instMulOneClass Units.instMulOneClass MonoidWithZero.toMulZeroOneClass funLike snd	—	snd_inr

---

← Back to Index