Commit 2025-01-27 22:45 31612cb1

View on Github →

feat(Algebra): Pi.single_induction (#21141) From "Formalizing the Bruhat-Tits tree"

Estimated changes

added theorem Pi.mulSingle_induction
added theorem Pi.single_induction