Range

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

Statistics

Metric	Count
Definitions ValueGroup₀, embedding, mk, restrict₀, ValueMonoid₀, instCommGroupWithZeroValueGroup₀, valueGroup, mk, valueMonoid	9
Theorems embedding_apply, embedding_restrict₀, mk_eq_of_ne_zero, restrict₀_apply, restrict₀_eq_one_iff, restrict₀_eq_zero_iff, restrict₀_of_ne_zero, restrict₀_range_eq_top, restrict₀_surjective, zero_or_exists_mk, zero_or_exists_mk', coe_one, inv_mem_valueGroup, mem_valueGroup, mem_valueGroup_iff_of_comm, mem_valueGroup_iff_of_comm', mem_valueMonoid, mem_valueMonoid_iff, mrange_nontrivial, one_mem_valueMonoid, range_nontrivial, mk_inj, mk_mul, valueGroup_def, valueGroup_eq_range, valueMonoid_eq_closure, valueMonoid_eq_valueGroup, valueMonoid_eq_valueGroup'	28
Total	37

MonoidWithZeroHom

Definitions

Name	Category	Theorems
ValueGroup₀ 📖	CompOp	126 math math: Valuation.mem_nhds_zero_iff, Valued.continuous_extension, Valued.isOpen_closedball, WithVal.valueGroupOrderIso₀_symm_apply, Valuation.isClopen_closedBall, Valued.extension_extends, ValueGroup₀.zero_or_exists_mk, WithVal.valueGroupOrderIso₀_restrict, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective, ValueGroup₀.monoidWithZeroHom_strictMono, WithVal.valueGroupOrderIso₀_apply, Valued.toUniformSpace_eq, NumberField.HeightOneSpectrum.rankOne_hom'_def, Valuation.restrict_eq_one_iff, Valuation.IsEquiv.restrict, Valued.isClopen_ball, ValuativeRel.ValueGroupWithZero.embed_strictMono, Valuation.hasBasis_nhds_zero, ValueGroup₀.restrict₀_eq_one_iff, ValuativeRel.ValueGroupWithZero.orderMonoidIso_valuation_eq_restrict₀, Valuation.restrict_le_iff, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_strictMono, Valued.is_topological_valuation, IsValuativeTopology.isOpen_ball, Valuation.restrict_eq_zero_iff, Valuation.restrict_eq_mk, ValuativeRel.ValueGroupWithZero.leftInverse_embedding_orderMonoidIso, Valued.continuous_valuation, Valuation.restrict_lt_iff_lt_embedding, Valued.extension_eq_zero_iff, ValueGroup₀.embedding_unit_pos, IsValuativeTopology.isClopen_sphere, ValueGroup₀.restrict₀_of_ne_zero, Valuation.subgroups_basis, Valued.isOpen_sphere, Valuation.restrict_le_iff_le_embedding, NumberField.HeightOneSpectrum.NumberField.rankOne_hom'_def, Valuation.isEquiv_restrict, Valuation.nonempty_rankOne_iff_mulArchimedean, Valuation.RankOne.exists_val_lt, Valued.hasBasis_nhds_zero, WithVal.strictMono_valueGroupOrderIso₀, WithVal.strictMono_valueGroupOrderIso₀_symm, Valuation.RankOne.strictMono, ValuativeRel.ValueGroupWithZero.embed_valuation_eq_restrict₀, Valued.coe_valuation_eq_rankOne_hom_comp_valuation, ValuativeRel.ValueGroupWithZero.orderMonoidIso_mk, ValueGroup₀.restrict₀_range_eq_top, Valued.isClosed_ball, Valuation.restrict_lt_one_iff, ValueGroup₀.embedding_apply, Valued.isClopen_sphere, Valued.isClosed_sphere, IsValuativeTopology.isClosed_closedBall, Valuation.cauchy_iff, Valuation.IsRankOneDiscrete.embedding_generator', ValuativeRel.ValueGroupWithZero.orderMonoidIso_embed, Valuation.restrict_inj, ValueGroup₀.restrict₀_eq_zero_iff, Valuation.embedding_restrict, Valued.valuation_isClosedMap, Valued.cauchy_iff, Valuation.restrict_pos_iff, IsValuativeTopology.isClopen_ball, Valuation.restrict_def, ValueGroup₀.restrict₀_surjective, Valuation.IsEquiv.orderMonoidIso_trans, Valuation.isClosed_closedBall, IsValuativeTopology.isOpen_closedBall, Valuation.toTopologicalSpace_eq, Valuation.isClopen_ball, Valued.isOpen_closedBall, Valuation.hasBasis_nhds, Valued.mem_nhds_zero, Valuation.RankLeOne.exists_val_lt, Valued.isOpen_ball, Valued.mem_nhds, Valuation.isOpen_ball, ValuativeRel.ValueGroupWithZero.embed_mk, IsValuativeTopology.isClosed_ball, WithVal.valueGroupOrderIso₀_symm_restrict, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_symm_apply, ValuativeRel.ValueGroupWithZero.embedding_orderMonoidIso_valuation_eq, Valuation.hasBasis_uniformity, Valued.toNormedField.norm_def, Valuation.toUniformSpace_eq, Valuation.isOpen_sphere, Valuation.norm_def, Valuation.exists_div_eq_of_unit, Valuation.restrict_le_one_iff, Valuation.isClosed_ball, Valuation.IsEquiv.orderMonoidIso_eq_refl, Valuation.RankOne.zero_of_hom_zero, ValueGroup₀.embedding_restrict₀, Valuation.IsEquiv.valueGroup₀Fun_zero, Valued.hasBasis_uniformity, ValuativeRel.valuation_lt_symm_orderMonoidIso, ValueGroup₀.restrict₀_apply, Valuation.restrict_lt_iff, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_apply, ValueGroup₀.zero_or_exists_mk', Valued.isClosed_closedBall, Valuation.isOpen_closedBall, Valuation.RankOne.isNontrivial_restrict, ValuativeRel.ValueGroupWithZero.embedding_embed_valuation_eq, ValuativeRel.restrict_lt_orderMonoidIso, Valuation.restrict_exists_div_eq, Valuation.IsEquiv.orderMonoidIso_spec, Valuation.RankOne.hom_eq_zero_iff, Valued.isClopen_closedBall, Valuation.RankOne.restrict_RankOne_hom_eq, ValueGroup₀.instIsOrderedMonoid, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_apply_zero, Valuation.RankLeOne.strictMono', Valuation.exists_setOf_restrict_le_iff, ValuativeRel.ValueGroupWithZero.orderMonoidIso_strictMono, IsValuativeTopology.isOpen_sphere, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_apply_zpow, ValueGroup₀.embedding_strictMono, IsValuativeTopology.isClopen_closedBall, Valuation.mem_nhds_iff, Valuation.is_topological_valuation, Valuation.isClopen_sphere, Valuation.IsEquiv.orderMonoidIso_symm, Valuation.isClosed_sphere, Valued.extensionValuation_toFun
ValueMonoid₀ 📖	CompOp	—
instCommGroupWithZeroValueGroup₀ 📖	CompOp	—
valueGroup 📖	CompOp	137 math math: Valuation.mem_nhds_zero_iff, Valued.isOpen_closedball, mem_valueGroup, WithVal.valueGroupOrderIso₀_symm_apply, Valuation.isClopen_closedBall, WithVal.valueGroup_eq, Valuation.IsRankOneDiscrete.exists_generator_lt_one', ValueGroup₀.zero_or_exists_mk, WithVal.valueGroupOrderIso₀_restrict, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective, Valuation.IsRankOneDiscrete.generator_mem_valueGroup, ValueGroup₀.monoidWithZeroHom_strictMono, WithVal.valueGroupOrderIso₀_apply, Valued.toUniformSpace_eq, NumberField.HeightOneSpectrum.rankOne_hom'_def, WithVal.valueGroupEquiv_symm_apply, Valuation.restrict_eq_one_iff, Valuation.IsRankOneDiscrete.generator'_lt_one, valueGroup.mk_mul, Valued.isClopen_ball, ValuativeRel.ValueGroupWithZero.embed_strictMono, Valuation.hasBasis_nhds_zero, ValueGroup₀.restrict₀_eq_one_iff, Valuation.IsUniformizer.zpowers_eq_valueGroup, ValuativeRel.ValueGroupWithZero.orderMonoidIso_valuation_eq_restrict₀, Valuation.restrict_le_iff, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_strictMono, Valued.is_topological_valuation, IsValuativeTopology.isOpen_ball, Valuation.restrict_eq_zero_iff, Valuation.restrict_eq_mk, ValuativeRel.ValueGroupWithZero.leftInverse_embedding_orderMonoidIso, Valuation.restrict_lt_iff_lt_embedding, Valued.extension_eq_zero_iff, ValueGroup₀.embedding_unit_pos, ValueGroup₀.restrict₀_of_ne_zero, Valuation.subgroups_basis, Valuation.restrict_le_iff_le_embedding, valueMonoid_eq_valueGroup, NumberField.HeightOneSpectrum.NumberField.rankOne_hom'_def, Valuation.nonempty_rankOne_iff_mulArchimedean, Valuation.RankOne.exists_val_lt, valueGroup_eq_range, Valued.hasBasis_nhds_zero, Valuation.IsRankOneDiscrete.instIsCyclicSubtypeUnitsMemSubgroupValueGroup, WithVal.strictMono_valueGroupOrderIso₀, WithVal.strictMono_valueGroupOrderIso₀_symm, WithVal.valueGroupEquiv_apply, Valuation.RankOne.strictMono, ValuativeRel.ValueGroupWithZero.embed_valuation_eq_restrict₀, Valued.coe_valuation_eq_rankOne_hom_comp_valuation, ValuativeRel.ValueGroupWithZero.orderMonoidIso_mk, ValueGroup₀.restrict₀_range_eq_top, Valued.isClosed_ball, Valuation.restrict_lt_one_iff, ValueGroup₀.embedding_apply, IsValuativeTopology.isClosed_closedBall, Valuation.IsRankOneDiscrete.valueGroup_genLTOne_eq_generator, Valuation.cauchy_iff, Valuation.IsRankOneDiscrete.embedding_generator', ValuativeRel.ValueGroupWithZero.orderMonoidIso_embed, ValueGroup₀.restrict₀_eq_zero_iff, Valuation.embedding_restrict, ValueGroup₀.mk_eq_of_ne_zero, Valued.cauchy_iff, Valuation.IsRankOneDiscrete.generator'_zpowers_eq_top, mem_valueGroup_iff_of_comm', Valuation.restrict_pos_iff, IsValuativeTopology.isClopen_ball, Valuation.restrict_def, ValueGroup₀.restrict₀_surjective, Valuation.IsEquiv.orderMonoidIso_trans, WithVal.strictMono_valueGroupEquiv_symm, Valuation.IsRankOneDiscrete.generator_zpowers_eq_valueGroup, Valuation.isClosed_closedBall, IsValuativeTopology.isOpen_closedBall, Valuation.toTopologicalSpace_eq, Valuation.isClopen_ball, Valued.isOpen_closedBall, Valuation.instNontrivialSubtypeUnitsMemSubgroupValueGroupOfIsNontrivial, Valuation.hasBasis_nhds, valueGroup_def, Valued.mem_nhds_zero, Valuation.RankLeOne.exists_val_lt, Valued.isOpen_ball, Valued.mem_nhds, Valuation.isOpen_ball, ValuativeRel.ValueGroupWithZero.embed_mk, valueMonoid_eq_valueGroup', IsValuativeTopology.isClosed_ball, WithVal.valueGroupOrderIso₀_symm_restrict, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_symm_apply, ValuativeRel.ValueGroupWithZero.embedding_orderMonoidIso_valuation_eq, Valuation.hasBasis_uniformity, Valued.toNormedField.norm_def, Valuation.toUniformSpace_eq, Valuation.norm_def, Valuation.exists_div_eq_of_unit, Valuation.restrict_le_one_iff, Valuation.isClosed_ball, mem_valueGroup_iff_of_comm, Valuation.IsEquiv.orderMonoidIso_eq_refl, Valuation.RankOne.zero_of_hom_zero, ValueGroup₀.embedding_restrict₀, IsDedekindDomain.HeightOneSpectrum.adicCompletion_valueGroup_eq, Valuation.IsEquiv.valueGroup₀Fun_zero, Valuation.IsEquiv.valueGroup₀Fun_spec, Valued.hasBasis_uniformity, ValuativeRel.valuation_lt_symm_orderMonoidIso, ValueGroup₀.restrict₀_apply, Valuation.restrict_lt_iff, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_apply, ValueGroup₀.zero_or_exists_mk', Valued.isClosed_closedBall, Valuation.isOpen_closedBall, ValuativeRel.ValueGroupWithZero.embedding_embed_valuation_eq, ValuativeRel.restrict_lt_orderMonoidIso, inv_mem_valueGroup, Valuation.restrict_exists_div_eq, Valuation.IsEquiv.orderMonoidIso_spec, Valuation.RankOne.hom_eq_zero_iff, Valued.isClopen_closedBall, Valuation.RankOne.restrict_RankOne_hom_eq, WithVal.strictMono_valueGroupEquiv, ValueGroup₀.instIsOrderedMonoid, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_apply_zero, Valuation.RankLeOne.strictMono', Valuation.exists_setOf_restrict_le_iff, ValuativeRel.ValueGroupWithZero.orderMonoidIso_strictMono, Valuation.IsRankOneDiscrete.exists_generator_lt_one, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_apply_zpow, ValueGroup₀.embedding_strictMono, IsValuativeTopology.isClopen_closedBall, Valuation.mem_nhds_iff, Valuation.is_topological_valuation, Valuation.IsEquiv.orderMonoidIso_symm, Valued.extensionValuation_toFun
valueMonoid 📖	CompOp	9 math math: Valuation.instNontrivialSubtypeUnitsMemSubmonoidValueMonoidOfIsNontrivial, coe_one, mem_valueMonoid, valueMonoid_eq_valueGroup, valueGroup_def, valueMonoid_eq_closure, valueMonoid_eq_valueGroup', one_mem_valueMonoid, mem_valueMonoid_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_one 📖	mathematical	—	Units MonoidWithZero.toMonoid Submonoid Units.instMulOneClass SetLike.instMembership Submonoid.instSetLike valueMonoid Units.instOne one_mem_valueMonoid Submonoid.one	—	one_mem_valueMonoid
inv_mem_valueGroup 📖	mathematical	Set Set.instMembership Set.range DFunLike.coe Units.val MonoidWithZero.toMonoid	Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike valueGroup Units.instInv	—	Subgroup.inv_mem mem_valueGroup
mem_valueGroup 📖	mathematical	Set Set.instMembership Set.range DFunLike.coe Units.val MonoidWithZero.toMonoid	Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike valueGroup	—	mem_valueMonoid Subgroup.mem_closure
mem_valueGroup_iff_of_comm 📖	mathematical	—	Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike valueGroup MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass DFunLike.coe Units.val	—	Subgroup.closure_induction Units.ne_zero GroupWithZero.toNontrivial map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass map_one MonoidHomClass.toOneHomClass NeZero.one mul_one GroupWithZero.noZeroDivisors mul_mul_mul_comm Units.val_inv_eq_inv_val mul_inv_cancel_right₀ Ne.isUnit IsUnit.unit_spec inv_mul_eq_iff_eq_mul Subgroup.mul_mem inv_mem_valueGroup mem_valueGroup
mem_valueGroup_iff_of_comm' 📖	mathematical	—	Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike valueGroup MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass DFunLike.coe Units.val	—	mem_valueGroup_iff_of_comm GroupWithZero.noZeroDivisors GroupWithZero.toNontrivial
mem_valueMonoid 📖	mathematical	Set Set.instMembership Set.range DFunLike.coe Units.val MonoidWithZero.toMonoid	Units MonoidWithZero.toMonoid Submonoid Units.instMulOneClass SetLike.instMembership Submonoid.instSetLike valueMonoid	—	—
mem_valueMonoid_iff 📖	mathematical	—	Units MonoidWithZero.toMonoid Submonoid Units.instMulOneClass SetLike.instMembership Submonoid.instSetLike valueMonoid Set Set.instMembership Set.preimage Units.val Set.range DFunLike.coe	—	—
mrange_nontrivial 📖	mathematical	—	Nontrivial Submonoid MulZeroOneClass.toMulOneClass SetLike.instMembership Submonoid.instSetLike MonoidHom.mrange MonoidWithZeroHom funLike MonoidWithZeroHomClass.toMonoidHomClass monoidWithZeroHomClass	—	MonoidWithZeroHomClass.toMonoidHomClass monoidWithZeroHomClass NeZero.one
one_mem_valueMonoid 📖	mathematical	—	Units MonoidWithZero.toMonoid Submonoid Units.instMulOneClass SetLike.instMembership Submonoid.instSetLike valueMonoid Units.instOne	—	map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass
range_nontrivial 📖	mathematical	—	Set.Nontrivial Set.range DFunLike.coe MonoidWithZeroHom funLike	—	Set.nontrivial_coe_sort mrange_nontrivial
valueGroup_def 📖	mathematical	—	valueGroup Subgroup.closure Units MonoidWithZero.toMonoid Units.instGroup SetLike.coe Submonoid Units.instMulOneClass Submonoid.instSetLike valueMonoid	—	—
valueGroup_eq_range 📖	mathematical	—	Set.image Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero Units.val SetLike.coe Subgroup Units.instGroup Subgroup.instSetLike valueGroup Set Set.instSDiff Set.range DFunLike.coe Set.instSingletonSet MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass	—	Set.ext valueMonoid_eq_valueGroup' GroupWithZero.toNontrivial
valueMonoid_eq_closure 📖	mathematical	—	valueMonoid Submonoid.closure Units MonoidWithZero.toMonoid Units.instMulOneClass Set.preimage Units.val Set.range DFunLike.coe	—	Submonoid.closure_eq
valueMonoid_eq_valueGroup 📖	mathematical	—	valueMonoid GroupWithZero.toMonoidWithZero Subgroup.toSubmonoid Units MonoidWithZero.toMonoid Units.instGroup valueGroup	—	valueGroup_def Subgroup.closure_toSubmonoid Submonoid.closure_eq_of_le Set.instReflSubset map_inv₀ Units.val_inv_eq_inv_val inv_inv Submonoid.closure_union Submonoid.closure_eq
valueMonoid_eq_valueGroup' 📖	mathematical	—	SetLike.coe Submonoid Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero Units.instMulOneClass Submonoid.instSetLike valueMonoid Subgroup Units.instGroup Subgroup.instSetLike valueGroup	—	valueMonoid_eq_valueGroup Subgroup.coe_toSubmonoid

MonoidWithZeroHom.ValueGroup₀

Definitions

Name	Category	Theorems
embedding 📖	CompOp	18 math math: Valued.toUniformSpace_eq, ValuativeRel.ValueGroupWithZero.leftInverse_embedding_orderMonoidIso, Valuation.restrict_lt_iff_lt_embedding, embedding_unit_pos, Valuation.subgroups_basis, Valuation.restrict_le_iff_le_embedding, embedding_apply, Valuation.IsRankOneDiscrete.embedding_generator', Valuation.embedding_restrict, Valuation.toTopologicalSpace_eq, PadicComplex.RankOne.hom_eq_embedding, ValuativeRel.ValueGroupWithZero.embedding_orderMonoidIso_valuation_eq, Valuation.toUniformSpace_eq, embedding_restrict₀, ValuativeRel.ValueGroupWithZero.embedding_embed_valuation_eq, Valuation.RankOne.restrict_RankOne_hom_eq, embedding_strictMono, Valued.extensionValuation_toFun
mk 📖	CompOp	—
restrict₀ 📖	CompOp	12 math math: restrict₀_eq_one_iff, ValuativeRel.ValueGroupWithZero.orderMonoidIso_valuation_eq_restrict₀, restrict₀_of_ne_zero, ValuativeRel.ValueGroupWithZero.embed_valuation_eq_restrict₀, ValuativeRel.ValueGroupWithZero.orderMonoidIso_mk, restrict₀_range_eq_top, restrict₀_eq_zero_iff, Valuation.restrict_def, restrict₀_surjective, ValuativeRel.ValueGroupWithZero.embed_mk, embedding_restrict₀, restrict₀_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
embedding_apply 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom MonoidWithZeroHom.ValueGroup₀ GroupWithZero.toMonoidWithZero WithZero.instMulZeroOneClass Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MonoidWithZero.toMulZeroOneClass MonoidWithZeroHom.funLike embedding WithZero.recZeroCoe MulZeroClass.toZero MulZeroOneClass.toMulZeroClass Units.val WithZero Units.instMulOneClass WithZero.map' Subgroup.subtype	—	—
embedding_restrict₀ 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom MonoidWithZeroHom.ValueGroup₀ GroupWithZero.toMonoidWithZero WithZero.instMulZeroOneClass Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MonoidWithZero.toMulZeroOneClass MonoidWithZeroHom.funLike embedding restrict₀	—	map_zero MonoidWithZeroHomClass.toZeroHomClass MonoidWithZeroHom.monoidWithZeroHomClass
mk_eq_of_ne_zero 📖	mathematical	—	WithZero.coe Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup	—	—
restrict₀_apply 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom MonoidWithZeroHom.ValueGroup₀ GroupWithZero.toMonoidWithZero MonoidWithZero.toMulZeroOneClass WithZero.instMulZeroOneClass Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MonoidWithZeroHom.funLike restrict₀ MulZeroClass.toZero MulZeroOneClass.toMulZeroClass Classical.decPred WithZero.instZero WithZero.coe	—	—
restrict₀_eq_one_iff 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom MonoidWithZeroHom.ValueGroup₀ GroupWithZero.toMonoidWithZero MonoidWithZero.toMulZeroOneClass WithZero.instMulZeroOneClass Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MonoidWithZeroHom.funLike restrict₀ WithZero.one Subgroup.one InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	NeZero.one GroupWithZero.toNontrivial
restrict₀_eq_zero_iff 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom MonoidWithZeroHom.ValueGroup₀ GroupWithZero.toMonoidWithZero MonoidWithZero.toMulZeroOneClass WithZero.instMulZeroOneClass Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MonoidWithZeroHom.funLike restrict₀ WithZero.instZero MulZeroClass.toZero MulZeroOneClass.toMulZeroClass	—	—
restrict₀_of_ne_zero 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom MonoidWithZeroHom.ValueGroup₀ GroupWithZero.toMonoidWithZero MonoidWithZero.toMulZeroOneClass WithZero.instMulZeroOneClass Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MonoidWithZeroHom.funLike restrict₀ WithZero.coe MonoidWithZeroHom.mem_valueGroup Units.val	—	MonoidWithZeroHom.mem_valueGroup
restrict₀_range_eq_top 📖	mathematical	—	Set.range MonoidWithZeroHom.ValueGroup₀ GroupWithZero.toMonoidWithZero DFunLike.coe MonoidWithZeroHom MonoidWithZero.toMulZeroOneClass WithZero.instMulZeroOneClass Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MonoidWithZeroHom.funLike restrict₀ Top.top Set BooleanAlgebra.toTop Set.instBooleanAlgebra	—	Set.top_eq_univ Set.range_eq_univ map_zero MonoidWithZeroHomClass.toZeroHomClass MonoidWithZeroHom.monoidWithZeroHomClass MonoidWithZeroHom.valueMonoid_eq_valueGroup' GroupWithZero.toNontrivial
restrict₀_surjective 📖	mathematical	—	MonoidWithZeroHom.ValueGroup₀ GroupWithZero.toMonoidWithZero DFunLike.coe MonoidWithZeroHom MonoidWithZero.toMulZeroOneClass WithZero.instMulZeroOneClass Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MonoidWithZeroHom.funLike restrict₀	—	Set.mem_range restrict₀_range_eq_top
zero_or_exists_mk 📖	mathematical	—	MonoidWithZeroHom.ValueGroup₀ GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero WithZero.instZero Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup DFunLike.coe MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass WithZero.coe	—	MonoidWithZeroHom.mem_valueGroup_iff_of_comm' eq_inv_mul_iff_mul_eq mul_ne_zero_iff GroupWithZero.noZeroDivisors mul_comm
zero_or_exists_mk' 📖	mathematical	—	MonoidWithZeroHom.ValueGroup₀ GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero WithZero.instZero Units MonoidWithZero.toMonoid Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup DFunLike.coe MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass WithZero.coe	—	—

MonoidWithZeroHom.valueGroup

Definitions

Name	Category	Theorems
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_inj 📖	mathematical	—	DFunLike.coe MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass	—	map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass inv_mul_eq_inv_mul_iff_mul_eq_mul mul_comm
mk_mul 📖	mathematical	—	Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike MonoidWithZeroHom.valueGroup Subgroup.mul MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass	—	mul_ne_zero_iff GroupWithZero.noZeroDivisors map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass MulMemClass.mul_mem SubmonoidClass.toMulMemClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass mul_mul_mul_comm mul_inv

---

← Back to Index