Def direct_sum.is_internal.subordinate_orthonormal_basis_index
Modification history
2023-01-16 13:27
src/analysis/inner_product_space/pi_L2.lean
chore(*): remove after the fact attribute [irreducible] at several places (2) (#18180) …
Modified direct_sum.is_internal.subordinate_orthonormal_basis_indexView on Github →