Commit 2024-07-01 13:36 67a63ca3

View on Github →

chore: namespace some IsSelfAdjoint lemmas (#14211) Per this Zulip discussion we choose to namespace (and protect) a few lemmas about IsSelfAdjoint.

Estimated changes

Modified Mathlib/Algebra/Star/Order.lean

Modified Mathlib/Algebra/Star/SelfAdjoint.lean

added theorem IsSelfAdjoint.add_star_self

added theorem IsSelfAdjoint.star_add_self

deleted theorem isSelfAdjoint_add_star_self

deleted theorem isSelfAdjoint_intCast

deleted theorem isSelfAdjoint_natCast

deleted theorem isSelfAdjoint_nnratCast

deleted theorem isSelfAdjoint_ofNat

deleted theorem isSelfAdjoint_one

deleted theorem isSelfAdjoint_ratCast

deleted theorem isSelfAdjoint_star_add_self

deleted theorem isSelfAdjoint_zero

Modified Mathlib/Analysis/InnerProductSpace/Positive.lean

Modified Mathlib/Analysis/NormedSpace/Star/ContinuousFunctionalCalculus/Instances.lean

Modified Mathlib/LinearAlgebra/Matrix/Hermitian.lean