Commit 2025-07-10 19:37 3cbe35f8

View on Github →

chore(Gram-Schmidt): small tweaks (#26894)

improve formatting of the module doc-string
move all declarations to the InnerProductSpace namespace

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean

added theorem InnerProductSpace.coe_gramSchmidtBasis

added theorem InnerProductSpace.gramSchmidtNormed_orthonormal'

added theorem InnerProductSpace.gramSchmidtNormed_orthonormal

added theorem InnerProductSpace.gramSchmidtNormed_unit_length'

added theorem InnerProductSpace.gramSchmidtNormed_unit_length

added theorem InnerProductSpace.gramSchmidtNormed_unit_length_coe

added theorem InnerProductSpace.gramSchmidtOrthonormalBasis_apply

added theorem InnerProductSpace.gramSchmidtOrthonormalBasis_apply_of_orthogonal

added theorem InnerProductSpace.gramSchmidtOrthonormalBasis_det

added theorem InnerProductSpace.gramSchmidtOrthonormalBasis_inv_blockTriangular

added theorem InnerProductSpace.gramSchmidtOrthonormalBasis_inv_triangular'

added theorem InnerProductSpace.gramSchmidtOrthonormalBasis_inv_triangular

added theorem InnerProductSpace.gramSchmidt_def''

added theorem InnerProductSpace.gramSchmidt_def'

added theorem InnerProductSpace.gramSchmidt_def

added theorem InnerProductSpace.gramSchmidt_inv_triangular

added theorem InnerProductSpace.gramSchmidt_linearIndependent

added theorem InnerProductSpace.gramSchmidt_mem_span

added theorem InnerProductSpace.gramSchmidt_ne_zero

added theorem InnerProductSpace.gramSchmidt_ne_zero_coe

added theorem InnerProductSpace.gramSchmidt_of_orthogonal

added theorem InnerProductSpace.gramSchmidt_orthogonal

added theorem InnerProductSpace.gramSchmidt_pairwise_orthogonal

added theorem InnerProductSpace.gramSchmidt_triangular

added theorem InnerProductSpace.gramSchmidt_zero

added theorem InnerProductSpace.inner_gramSchmidtOrthonormalBasis_eq_zero

added theorem InnerProductSpace.mem_span_gramSchmidt

added theorem InnerProductSpace.span_gramSchmidt

added theorem InnerProductSpace.span_gramSchmidtNormed

added theorem InnerProductSpace.span_gramSchmidtNormed_range

added theorem InnerProductSpace.span_gramSchmidt_Iic

added theorem InnerProductSpace.span_gramSchmidt_Iio

deleted theorem coe_gramSchmidtBasis

deleted theorem gramSchmidtNormed_unit_length'

deleted theorem gramSchmidtNormed_unit_length

deleted theorem gramSchmidtNormed_unit_length_coe

deleted theorem gramSchmidtOrthonormalBasis_apply

deleted theorem gramSchmidtOrthonormalBasis_apply_of_orthogonal

deleted theorem gramSchmidtOrthonormalBasis_det

deleted theorem gramSchmidtOrthonormalBasis_inv_blockTriangular

deleted theorem gramSchmidtOrthonormalBasis_inv_triangular'

deleted theorem gramSchmidtOrthonormalBasis_inv_triangular

deleted theorem gramSchmidt_def''

deleted theorem gramSchmidt_def'

deleted theorem gramSchmidt_def

deleted theorem gramSchmidt_inv_triangular

deleted theorem gramSchmidt_linearIndependent

deleted theorem gramSchmidt_mem_span

deleted theorem gramSchmidt_ne_zero

deleted theorem gramSchmidt_ne_zero_coe

deleted theorem gramSchmidt_of_orthogonal

deleted theorem gramSchmidt_orthogonal

deleted theorem gramSchmidt_orthonormal'

deleted theorem gramSchmidt_orthonormal

deleted theorem gramSchmidt_pairwise_orthogonal

deleted theorem gramSchmidt_triangular

deleted theorem gramSchmidt_zero

deleted theorem inner_gramSchmidtOrthonormalBasis_eq_zero

deleted theorem mem_span_gramSchmidt

deleted theorem span_gramSchmidt

deleted theorem span_gramSchmidtNormed

deleted theorem span_gramSchmidtNormed_range

deleted theorem span_gramSchmidt_Iic

deleted theorem span_gramSchmidt_Iio

Modified Mathlib/Analysis/InnerProductSpace/Orientation.lean

Modified Mathlib/LinearAlgebra/Matrix/LDL.lean

Modified docs/undergrad.yaml