Range

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

Statistics

Metric	Count
Definitions ValueGroup₀, ValueMonoid₀, instCommGroupWithZeroValueGroup₀, valueGroup, valueGroup₀, valueMonoid, valueMonoid₀	7
Theorems coe_one, inv_mem_valueGroup, mem_valueGroup, mem_valueGroup_iff_of_comm, mem_valueMonoid, mem_valueMonoid_iff, mrange_nontrivial, one_mem_valueMonoid, range_nontrivial, valueGroup_def, valueGroup_eq_range, valueMonoid_eq_closure, valueMonoid_eq_valueGroup, valueMonoid_eq_valueGroup'	14
Total	21

MonoidWithZeroHom

Definitions

Name	Category	Theorems
ValueGroup₀ 📖	CompOp	—
ValueMonoid₀ 📖	CompOp	—
instCommGroupWithZeroValueGroup₀ 📖	CompOp	—
valueGroup 📖	CompOp	15 math math: mem_valueGroup, Valuation.IsRankOneDiscrete.exists_generator_lt_one', Valuation.IsRankOneDiscrete.generator_mem_valueGroup, Valuation.IsUniformizer.zpowers_eq_valueGroup, valueMonoid_eq_valueGroup, valueGroup_eq_range, Valuation.IsRankOneDiscrete.instIsCyclicSubtypeUnitsMemSubgroupValueGroup, Valuation.IsRankOneDiscrete.valueGroup_genLTOne_eq_generator, Valuation.IsRankOneDiscrete.generator_zpowers_eq_valueGroup, Valuation.instNontrivialSubtypeUnitsMemSubgroupValueGroupOfIsNontrivial, valueGroup_def, valueMonoid_eq_valueGroup', mem_valueGroup_iff_of_comm, inv_mem_valueGroup, Valuation.IsRankOneDiscrete.exists_generator_lt_one
valueGroup₀ 📖	CompOp	—
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
valueMonoid₀ 📖	CompOp	—

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 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 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_valueMonoid 📖	mathematical	Set Set.instMembership Set.range DFunLike.coe Units.val MonoidWithZero.toMonoid	Units 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

---

← Back to Index