2026-03-25 13:07
Mathlib/Analysis/Convex/Cone/TensorProduct.lean
feat(Analysis/Convex/Cone): min and max tensor products are equal when one factor is simplicial and generating (#34848) …
Added PointedCone.minTensorProduct_eq_max_of_simplicial_generating_right