Commit 2024-02-14 10:22 b94dc689

View on Github →

feat(GroupTheory/Submonoid/Units): Add Submonoid.units and related definitions and lemmas. (#9006) The subgroup of the type of units added in this PR is something we have in other guises, which are somewhat less useful for some forms of working. The intention is to provide different options depending on how you want to think about the group of units in a submonoid.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Units/Equiv.lean

deleted theorem coe_toUnits

added theorem toUnits_val_apply

Modified Mathlib/Analysis/Convolution.lean

Modified Mathlib/GroupTheory/Submonoid/Inverses.lean

Modified Mathlib/GroupTheory/Submonoid/Operations.lean

Created Mathlib/GroupTheory/Submonoid/Units.lean

added theorem Subgroup.exists_mem_ofUnits_val_eq

added theorem Subgroup.isUnit_of_mem_ofUnits

added theorem Subgroup.mem_iff_toUnits_mem_units

added theorem Subgroup.mem_ofUnits

added theorem Subgroup.mem_ofUnits_iff

added theorem Subgroup.mem_ofUnits_iff_exists_isUnit

added theorem Subgroup.mem_ofUnits_iff_toUnits_mem

added theorem Subgroup.mem_ofUnits_of_isUnit_of_unit_mem

added theorem Subgroup.mem_of_mem_val_ofUnits

added theorem Subgroup.mem_units_iff_val_mem

added def Subgroup.ofUnits

added theorem Subgroup.ofUnits_bot

added theorem Subgroup.ofUnits_iSup

added theorem Subgroup.ofUnits_iSup₂

added theorem Subgroup.ofUnits_inf

added theorem Subgroup.ofUnits_inf_units

added theorem Subgroup.ofUnits_injective

added theorem Subgroup.ofUnits_le_ofUnits_iff

added theorem Subgroup.ofUnits_mono

added theorem Subgroup.ofUnits_right_inverse

added theorem Subgroup.ofUnits_sSup

added theorem Subgroup.ofUnits_strictMono

added theorem Subgroup.ofUnits_sup_units

added theorem Subgroup.unit_eq_unit_of_mem_ofUnits

added theorem Subgroup.unit_mem_of_mem_ofUnits

added theorem Subgroup.unit_of_mem_ofUnits_spec_eq_of_val_mem

added theorem Subgroup.unit_of_mem_ofUnits_spec_mem

added theorem Subgroup.unit_of_mem_ofUnits_spec_val_eq_of_mem

added def Subgroup.unitsEquivSelf

added theorem Subgroup.units_ofUnits_eq

added theorem Subgroup.val_mem_ofUnits_iff_mem

added theorem Submonoid.coe_inv_val_mul_coe_val

added theorem Submonoid.coe_val_mul_coe_inv_val

added theorem Submonoid.inv_mem_units

added theorem Submonoid.inv_mem_units_iff

added theorem Submonoid.inv_val_mem_of_mem_units

added theorem Submonoid.mem_units_iff

added theorem Submonoid.mem_units_of_val_mem_inv_val_mem

added theorem Submonoid.mk_inv_mul_mk_eq_one

added theorem Submonoid.mk_mul_mk_inv_eq_one

added theorem Submonoid.mul_mem_units

added theorem Submonoid.ofUnits_units_le

added def Submonoid.units

added def Submonoid.unitsEquivUnitsType

added theorem Submonoid.units_bot

added theorem Submonoid.units_iInf

added theorem Submonoid.units_iInf₂

added theorem Submonoid.units_inf

added theorem Submonoid.units_left_inverse

added theorem Submonoid.units_mono

added theorem Submonoid.units_sInf

added theorem Submonoid.units_surjective

added theorem Submonoid.units_top

added theorem Submonoid.val_mem_of_mem_units

added theorem ofUnits_le_iff_le_units

added theorem ofUnits_units_gc

added def ofUnits_units_gci