Commit 2024-07-04 03:49 90e41c5a

View on Github →

style(Mathlib/Algebra/ContinuedFractions/*): shorten names of declarations related to continued fractions (#13210) I'm constructing the homeomorphism between irrationals and Baire space using continued fractions, and found that names of declarations related to continued fractions are long. This PR shortens them e.g.: GeneralizedContinuedFraction -> GenContFract SimpleContinuedFraction -> SimpContFract ContinuedFraction -> ContFract GeneralizedContinuedFraction.denominators -> GenContFract.dens etc.

Estimated changes

added def ContFract
deleted def ContinuedFraction
added structure GenContFract.Pair
added structure GenContFract
deleted structure GeneralizedContinuedFraction
added def SimpContFract
added def ContFract.of
added structure GenContFract.IntFractPair
added theorem GenContFract.of_s_head
added theorem GenContFract.of_s_succ
added theorem GenContFract.of_s_tail