Theorem PointedCone.basis_coord_mem_dual

Modification history

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.basis_coord_mem_dualView on Github →