Theorem left_le_lineMap_iff_nonneg

Modification history

2025-09-22 15:22

Mathlib/LinearAlgebra/AffineSpace/Ordered.lean

feat(LinearAlgebra/AffineSpace/Ordered): add `lineMap_le_lineMap_iff_of_lt'` (#27257) …

Added left_le_lineMap_iff_nonneg View on Github →