Commit 2022-12-22 18:05 f5fe44eb

View on Github →

feat: port Algebra.Ring.Pi (#1151)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Ring/Pi.lean

added def Pi.constNonUnitalRingHom

added def Pi.constRingHom

added def Pi.evalNonUnitalRingHom

added def Pi.evalRingHom

added theorem Pi.nonUnitalRingHom_injective

added theorem Pi.ringHom_injective