Theorem GradedRingHom.toRingHom_eq_toRingHom

Modification history

2026-03-03 16:35
Mathlib/RingTheory/GradedAlgebra/RingHom.lean
feat(RingTheory): define graded ring homomorphisms (#30312) …
Added GradedRingHom.toRingHom_eq_toRingHomView on Github →