Theorem Function.subtypeNeLift_of_neq

Modification history

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