Commit 2024-12-20 20:04 3bc257ba

View on Github →

feat(GroupTheory/SemidirectProduct): Add various maps (#20102) This PR adds some more maps to GroupTheory/SemidirectProduct.lean.

Estimated changes

modified theorem SemidirectProduct.lift_inl
modified theorem SemidirectProduct.lift_inr
modified def SemidirectProduct.map
modified theorem SemidirectProduct.map_inl
modified theorem SemidirectProduct.map_inr
modified theorem SemidirectProduct.map_left
modified theorem SemidirectProduct.map_right