Theorem Function.subtypeNeLift_restriction

Modification history

2026-06-18 10:07
Mathlib/Data/SubtypeNeLift.lean
feat(LinearAlgebra): generators of pi tensor products (#26464) …
Added Function.subtypeNeLift_restrictionView on Github →