Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-11 13:28 9beec03c

View on Github →

feat(group_theory/subgroup): le_ker_iff (#6630) A subgroup is contained in the kernel iff it is mapped to the trivial subgroup.

Estimated changes

Modified src/algebra/lie/nilpotent.lean

Modified src/algebra/lie/solvable.lean

Modified src/algebra/lie/submodule.lean

deleted theorem lie_hom.map_bot_iff

added theorem lie_ideal.map_eq_bot_iff

Modified src/group_theory/solvable.lean

Modified src/group_theory/subgroup.lean

added theorem monoid_hom.ker_eq_bot_iff

modified theorem subgroup.map_eq_bot_iff

added theorem subgroup.map_eq_bot_iff_of_injective