Theorem GradedAlgHom.restrictScalars_coe_linearMap

Modification history

2026-03-06 15:35
Mathlib/RingTheory/GradedAlgebra/AlgHom.lean
feat(RingTheory): two constructions about base change and restriction of graded algebra (#36226) …
Added GradedAlgHom.restrictScalars_coe_linearMapView on Github →