Commit 2021-01-07 19:12 2894260b

View on Github →

feat(group_theory): add lemmas on solvability (#5646) Proves some basic lemmas about solvable groups: the subgroup of a solvable group is solvable, a quotient of a solvable group is solvable.

Estimated changes

Modified src/group_theory/solvable.lean

added theorem commutator_le_map_commutator

added theorem derived_series_le_map_derived_series

added theorem is_solvable_def

added theorem is_solvable_of_top_eq_bot

added theorem map_commutator_eq_commutator_map

added theorem map_derived_series_eq

added theorem map_derived_series_le_derived_series

added theorem solvable_of_solvable_injective

added theorem solvable_of_surjective

Modified src/group_theory/subgroup.lean

added theorem subgroup.map_eq_bot_iff