Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-05 08:10 4912740a

View on Github →

chore(analysis/inner_product_space/basic): extract common variables (#11214)

Estimated changes

Modified src/analysis/inner_product_space/basic.lean

modified theorem direct_sum.submodule_is_internal.collected_basis_orthonormal

modified theorem orthogonal_family.comp

modified theorem orthogonal_family.eq_ite

modified theorem orthogonal_family.independent

modified theorem orthogonal_family.inner_right_dfinsupp

modified theorem orthogonal_family.inner_right_fintype

modified theorem orthogonal_family.orthonormal_sigma_orthonormal