Commit 2023-02-08 11:21 9ec2a6f6

View on Github →

feat: port GroupTheory.Divisible (#2149)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Divisible.lean

added theorem AddCommGroup.smul_top_eq_top_of_divisibleBy_int

added def Group.rootableByIntOfRootableByNat

added def Group.rootableByNatOfRootableByInt

added theorem RootableBy.surjective_pow

added theorem pow_left_surj_of_rootableBy

Modified Mathlib/Tactic/ToAdditive.lean