Commit 2023-02-06 08:37 f7001b11

View on Github →

feat: port Algebra.Star.SelfAdjoint (#1860) See the Zulip thread for issues I encountered.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Star/SelfAdjoint.lean

added theorem IsSelfAdjoint.add

added theorem IsSelfAdjoint.bit0

added theorem IsSelfAdjoint.bit1

added theorem IsSelfAdjoint.conjugate'

added theorem IsSelfAdjoint.conjugate

added theorem IsSelfAdjoint.div

added theorem IsSelfAdjoint.inv

added theorem IsSelfAdjoint.isStarNormal

added theorem IsSelfAdjoint.mul

added theorem IsSelfAdjoint.mul_star_self

added theorem IsSelfAdjoint.neg

added theorem IsSelfAdjoint.pow

added theorem IsSelfAdjoint.smul

added theorem IsSelfAdjoint.starHom_apply

added theorem IsSelfAdjoint.star_eq

added theorem IsSelfAdjoint.star_iff

added theorem IsSelfAdjoint.star_mul_self

added theorem IsSelfAdjoint.sub

added theorem IsSelfAdjoint.zpow

added def IsSelfAdjoint

added theorem isSelfAdjoint_iff

added theorem isSelfAdjoint_one

added theorem isSelfAdjoint_zero

added theorem selfAdjoint.mem_iff

added theorem selfAdjoint.ratCast_mem

added theorem selfAdjoint.star_val_eq

added theorem selfAdjoint.val_div

added theorem selfAdjoint.val_inv

added theorem selfAdjoint.val_mul

added theorem selfAdjoint.val_one

added theorem selfAdjoint.val_pow

added theorem selfAdjoint.val_ratCast

added theorem selfAdjoint.val_rat_smul

added theorem selfAdjoint.val_smul

added theorem selfAdjoint.val_zpow

added def selfAdjoint

added theorem skewAdjoint.bit0_mem

added theorem skewAdjoint.conjugate'

added theorem skewAdjoint.conjugate

added theorem skewAdjoint.isStarNormal_of_mem

added theorem skewAdjoint.mem_iff

added theorem skewAdjoint.smul_mem

added theorem skewAdjoint.star_val_eq

added theorem skewAdjoint.val_smul

added def skewAdjoint

added theorem star_comm_self'