Commit 2023-04-15 20:36 e978148f

View on Github →

chore: forward port mathlib#18810, 18798, 18738 (#3443)

algebra.order.sub.defs, data.real.nnreal: leanprover-community/mathlib#18810, which is itself a backport. Also fixes a docstring typo.
linear_algebra.matrix.dot_product: leanprover-community/mathlib#18798
data.matrix.basic: leanprover-community/mathlib#18738

Estimated changes

Modified Mathlib/Algebra/Order/Sub/Defs.lean

Modified Mathlib/Data/Matrix/Basic.lean

added theorem Matrix.comp_equiv_dotProduct_comp_equiv

added theorem Matrix.comp_equiv_symm_dotProduct

added theorem Matrix.dotProduct_comp_equiv_symm

added theorem Matrix.reindex_updateColumn

added theorem Matrix.reindex_updateRow

added theorem Matrix.submatrix_mulVec_equiv

added theorem Matrix.submatrix_updateColumn_equiv

added theorem Matrix.submatrix_updateRow_equiv

added theorem Matrix.submatrix_vecMul_equiv

modified def Matrix.updateColumn

added theorem Matrix.updateColumn_reindex

added theorem Matrix.updateColumn_submatrix_equiv

added theorem Matrix.updateRow_reindex

added theorem Matrix.updateRow_submatrix_equiv

Modified Mathlib/Data/Real/NNReal.lean

Modified Mathlib/LinearAlgebra/Matrix/DotProduct.lean

modified theorem Matrix.dotProduct_self_star_eq_zero

modified theorem Matrix.dotProduct_star_self_eq_zero