Commit 2023-01-27 06:03 ace49f12

View on Github →

feat: Port RingTheory/RingInvo (#1276) Everything compiles properly, not done with style/removing unnecisary lemmas

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/RingInvo.lean

added theorem RingInvo.coe_ringEquiv

added theorem RingInvo.involution

added theorem RingInvo.map_eq_zero_iff

added def RingInvo.mk'

added structure RingInvo

added def RingInvoClass.toRingInvo