Commit 2022-12-26 16:03 471be08d

View on Github →

Revert "initial commit" This reverts commit 741d8e522c65874b883d55afe3019f40c6b476c2.

Estimated changes

Modified Mathlib.lean

Deleted Mathlib/Algebra/GroupRingAction/Basic.lean

deleted def MulSemiringAction.compHom

deleted def MulSemiringAction.toRingEquiv

deleted def MulSemiringAction.toRingHom

deleted theorem smul_inv''

deleted theorem to_ring_hom_injective