Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-19 21:39 0f6670b8

View on Github →

chore(group_theory/subgroup/basic): split out some self-contained sections (#17862) This is a very big file by mathlib standards at over 3000 lines. It seems helpful to reduce that by splitting some of the less fundamental definitions into their own files.

Estimated changes

added theorem subgroup.smul_def
deleted theorem int.mem_zmultiples_iff
deleted theorem monoid_hom.map_zpowers
deleted theorem subgroup.center_eq_infi'
deleted theorem subgroup.center_eq_infi
deleted theorem subgroup.exists_zpowers
deleted theorem subgroup.forall_zpowers
deleted theorem subgroup.mem_zpowers
deleted theorem subgroup.mem_zpowers_iff
deleted theorem subgroup.npow_mem_zpowers
deleted def subgroup.opposite
deleted def subgroup.saturated
deleted theorem subgroup.smul_def
deleted theorem subgroup.zpow_mem_zpowers
deleted def subgroup.zpowers
deleted theorem subgroup.zpowers_eq_bot
deleted theorem subgroup.zpowers_le
deleted theorem subgroup.zpowers_subset
added theorem int.mem_zmultiples_iff
added theorem monoid_hom.map_zpowers
added theorem subgroup.mem_zpowers
added def subgroup.zpowers
added theorem subgroup.zpowers_le