Theorem AlgHom.val_comp_rangeRestrict

Modification history

2025-12-14 12:40

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

feat(RingTheory/PolynomialLaw/Basic): extends polynomial laws to arbitrary universes (#26719) …

Added AlgHom.val_comp_rangeRestrict View on Github →