Commit 2024-01-07 10:52 83b4d8db

View on Github →

feat: Every star ring is a Nat-star module (#9470) and other basic star lemmas From LeanAPAP

Estimated changes

modified theorem RingHom.star_apply
modified theorem RingHom.star_def
added theorem conj_trivial
modified def starRingAut
modified def starRingEnd
modified theorem starRingEnd_apply
modified theorem starRingEnd_self_apply
added theorem Pi.conj_apply
added theorem IsSelfAdjoint.conj_eq
modified theorem isSelfAdjoint_one
modified theorem isSelfAdjoint_zero