Commit 2023-06-08 07:32 4d3d2de8

View on Github →

chore: forward-port leanprover-community/mathlib#18854 (#4840) This forward-ports all the files from leanprover-community/mathlib#18854 which have already been ported, and it also ports the new file algebra.star.order, which is a split from algebra.star.basic and was necessary to do at the same time.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/MonoidAlgebra/Grading.lean

Modified Mathlib/Algebra/Star/Basic.lean

deleted theorem conjugate_le_conjugate'

deleted theorem conjugate_le_conjugate

deleted theorem conjugate_nonneg'

deleted theorem conjugate_nonneg

deleted theorem star_mul_self_nonneg'

deleted theorem star_mul_self_nonneg

Modified Mathlib/Algebra/Star/CHSH.lean

Created Mathlib/Algebra/Star/Order.lean

added theorem StarOrderedRing.nonneg_iff

added def StarOrderedRing.ofLeIff

added def StarOrderedRing.ofNonnegIff'

added def StarOrderedRing.ofNonnegIff

added theorem conjugate_le_conjugate'

added theorem conjugate_le_conjugate

added theorem conjugate_nonneg'

added theorem conjugate_nonneg

added theorem star_mul_self_nonneg'

added theorem star_mul_self_nonneg

Modified Mathlib/Data/Complex/Basic.lean

Modified Mathlib/Data/Real/Sqrt.lean

Modified Mathlib/LinearAlgebra/Matrix/DotProduct.lean

Modified docs/references.bib