Commit 2024-11-19 17:43 fdc34d21

View on Github →

feat: IsSelfAdjoint.smul_iff (#19216) Also generalizes some typeclass assumptions from DivisionSemiring to GroupWithZero and renames a few declarations.

Estimated changes

Modified Mathlib/Algebra/Star/Basic.lean

deleted theorem star_div'

added theorem star_div₀

deleted theorem star_inv'

added theorem star_inv₀

modified theorem star_zpow₀

Modified Mathlib/Algebra/Star/Pointwise.lean

Modified Mathlib/Algebra/Star/SelfAdjoint.lean

added theorem IsSelfAdjoint.inv₀

modified theorem IsSelfAdjoint.smul

added theorem IsSelfAdjoint.smul_iff

added theorem IsSelfAdjoint.zpow₀

Modified Mathlib/Analysis/InnerProductSpace/Symmetric.lean

Modified Mathlib/Analysis/RCLike/Basic.lean

Modified Mathlib/Data/Complex/Basic.lean