OAI/Analysis/WeakInfiniteness/ScalarHereditary.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.WeakPureInfiniteness.map_mul_of_hereditary_squareline 33 - lemma
OAI.WeakPureInfiniteness.exists_real_scalar_of_no_orthogonalline 43