OAI/LinearAlgebra/MatrixMultiplication/JointExtraction/PopulationMixedNonzero.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Joint tensor extraction, compatibility and entropy estimates.

  1. theorem OAI.MatrixMultiplication.JointPopulationMixedNonzero.class_half_products_nonzero line 20