Def MulSemiringAction.toRingEquiv
Modification history
2026-06-20 09:31
Mathlib/Algebra/Ring/Action/Group.lean
refactor(RingTheory/Localization/FractionRing): remove bottom ring and field from `IsFractionRing.mulSemiringAction` (#40804) …
Modified MulSemiringAction.toRingEquivView on Github →2024-06-29 09:06
Mathlib/Algebra/Ring/Action/Basic.lean
chore: reduce imports on the path to LinearMap (#14246)
Modified MulSemiringAction.toRingEquivView on Github →2022-12-26 20:25
Mathlib/Algebra/GroupRingAction/Basic.lean
feat port: Algebra.GroupRingAction.Basic (#1225) …
Added MulSemiringAction.toRingEquivView on Github →