Commit 2022-12-26 16:00 741d8e52

View on Github →

initial commit

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