Theorem GroupExtension.Section.mul_inv_mul_mul_mem_range_inl

Modification history

2025-02-07 17:49
Mathlib/GroupTheory/GroupExtension/Basic.lean
chore(GroupExtension/Basic): add lemmas about extensions by (non-abelian) groups (#20998) …
Added GroupExtension.Section.mul_inv_mul_mul_mem_range_inlView on Github →