Commit 2024-04-09 20:56 61447777

View on Github →

feat: add induction principle for elementalStarAlgebra (#12039)

Estimated changes

Modified Mathlib/RingTheory/Adjoin/Basic.lean

added theorem Algebra.adjoin_induction''

Modified Mathlib/Topology/Algebra/StarSubalgebra.lean

added theorem elementalStarAlgebra.induction_on

added theorem elementalStarAlgebra.isClosed