Theorem GradedAlgHom.coe_monoidHom_injective

Modification history

2026-09-15 17:41

Mathlib/RingTheory/GradedAlgebra/AlgHom.lean

chore(Algebra/MonoidHom): rename to `.ofClass` (#43755) …

Deleted GradedAlgHom.coe_monoidHom_injective View on Github →

2026-03-05 14:29

Mathlib/RingTheory/GradedAlgebra/AlgHom.lean

feat(RingTheory): define R-linear graded algebra homomorphism (#30365) …

Added GradedAlgHom.coe_monoidHom_injective View on Github →