Mathlib v3 is deprecated. Go to Mathlib v4

Theorem subgroup.closure_induction_left

Modification history

2023-04-03 20:45
src/group_theory/subgroup/pointwise.lean
feat(algebra/group_power/lemmas): Induction principle for powers (#18668) …
Modified subgroup.closure_induction_leftView on Github →
2022-11-13 03:11
src/group_theory/subgroup/basic.lean
move(group_theory/group_action/*): Move pointwise subgroup operations (#17491) …
Modified subgroup.closure_induction_leftView on Github →
2022-03-17 11:06
src/group_theory/subgroup/basic.lean
feat(group_theory/subgroup/basic): One-sided closure induction lemmas (#12725) …
Added subgroup.closure_induction_leftView on Github →