Commit 2022-12-26 20:25 b06cedfb

View on Github →

feat port: Algebra.GroupRingAction.Basic (#1225) Easy

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/GroupRingAction/Basic.lean

added def MulSemiringAction.compHom

added def MulSemiringAction.toRingEquiv

added def MulSemiringAction.toRingHom

added theorem smul_inv''

added theorem to_ring_hom_injective