Commit 2023-01-26 13:42 06fce010

View on Github →

feat: port GroupTheory.Subgroup.Zpowers (#1852)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Subgroup/Zpowers.lean

added theorem AddSubgroup.int_cast_mem_zmultiples_one

added theorem AddSubgroup.int_cast_mul_mem_zmultiples

added theorem AddSubgroup.range_zmultiplesHom

added def AddSubgroup.zmultiples

added theorem Int.mem_zmultiples_iff

added theorem MonoidHom.map_zpowers

added theorem Subgroup.center_eq_infi'

added theorem Subgroup.center_eq_infᵢ

added theorem Subgroup.centralizer_closure

added theorem Subgroup.exists_mem_zpowers

added theorem Subgroup.exists_zpowers

added theorem Subgroup.forall_mem_zpowers

added theorem Subgroup.forall_zpowers

added theorem Subgroup.mem_zpowers

added theorem Subgroup.mem_zpowers_iff

added theorem Subgroup.npow_mem_zpowers

added theorem Subgroup.range_zpowersHom

added theorem Subgroup.zpow_mem_zpowers

added def Subgroup.zpowers

added theorem Subgroup.zpowers_eq_bot

added theorem Subgroup.zpowers_eq_closure

added theorem Subgroup.zpowers_le

added theorem Subgroup.zpowers_one_eq_bot

added theorem Subgroup.zpowers_subset

added theorem ofAdd_image_zmultiples_eq_zpowers_ofAdd

added theorem ofMul_image_zpowers_eq_zmultiples_ofMul