Theorem PolynomialLaw.exists_lift_of_mem_range_rTensor

Modification history

2025-12-14 12:40

Mathlib/RingTheory/PolynomialLaw/Basic.lean

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

Added PolynomialLaw.exists_lift_of_mem_range_rTensor View on Github →