Commit 2023-03-01 10:00 d1c1ae59

View on Github →

feat: port Algebra.Algebra.Pi (#2549)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Algebra/Pi.lean

added def AlgEquiv.piCongrRight

added theorem AlgEquiv.piCongrRight_refl

added theorem AlgEquiv.piCongrRight_symm

added theorem AlgEquiv.piCongrRight_trans

added theorem Pi.algebraMap_apply

added theorem Pi.algebraMap_def

added def Pi.constAlgHom

added theorem Pi.constAlgHom_eq_algebra_ofId

added theorem Pi.constRingHom_eq_algebraMap

added def Pi.evalAlgHom