Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-28 21:11 27ac3e1a

View on Github →

feat(algebra/star/basic): basic lemmas for star_ordered_ring (#17218)

Estimated changes

added theorem conjugate_le_conjugate
added theorem conjugate_nonneg'
added theorem conjugate_nonneg
modified theorem star_mul_self_nonneg'
modified theorem star_mul_self_nonneg