Commit 2023-01-28 19:02 35c97af4

View on Github →

feat:port GroupTheory.SemidirectProduct (#1878)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/SemidirectProduct.lean

added theorem SemidirectProduct.hom_ext

added def SemidirectProduct.inl

added theorem SemidirectProduct.inl_aut

added theorem SemidirectProduct.inl_aut_inv

added theorem SemidirectProduct.inl_inj

added theorem SemidirectProduct.inl_injective

added theorem SemidirectProduct.inl_left_mul_inr_right

added def SemidirectProduct.inr

added theorem SemidirectProduct.inr_inj

added theorem SemidirectProduct.inr_injective

added theorem SemidirectProduct.inv_left

added theorem SemidirectProduct.inv_right

added theorem SemidirectProduct.left_inl

added theorem SemidirectProduct.left_inr

added def SemidirectProduct.lift

added theorem SemidirectProduct.lift_comp_inl

added theorem SemidirectProduct.lift_comp_inr

added theorem SemidirectProduct.lift_inl

added theorem SemidirectProduct.lift_inr

added theorem SemidirectProduct.lift_unique

added def SemidirectProduct.map

added theorem SemidirectProduct.map_comp_inl

added theorem SemidirectProduct.map_comp_inr

added theorem SemidirectProduct.map_inl

added theorem SemidirectProduct.map_inr

added theorem SemidirectProduct.map_left

added theorem SemidirectProduct.map_right

added theorem SemidirectProduct.mk_eq_inl_mul_inr

added theorem SemidirectProduct.mul_def

added theorem SemidirectProduct.mul_left

added theorem SemidirectProduct.mul_right

added theorem SemidirectProduct.one_left

added theorem SemidirectProduct.one_right

added theorem SemidirectProduct.range_inl_eq_ker_rightHom

added def SemidirectProduct.rightHom

added theorem SemidirectProduct.rightHom_comp_inl

added theorem SemidirectProduct.rightHom_comp_inr

added theorem SemidirectProduct.rightHom_comp_map

added theorem SemidirectProduct.rightHom_eq_right

added theorem SemidirectProduct.rightHom_inl

added theorem SemidirectProduct.rightHom_inr

added theorem SemidirectProduct.rightHom_surjective

added theorem SemidirectProduct.right_inl

added theorem SemidirectProduct.right_inr

added structure SemidirectProduct