Commit 2023-01-13 14:42 a671aef1

View on Github →

chore: fix names in Xgcd.lean (#1540) I misapplied the naming conventions when reviewing the PR that ported this file. This PR fixes the capitalization of some Props.

Estimated changes

Modified Mathlib/Data/PNat/Xgcd.lean

added def PNat.XgcdType.IsReduced'

added def PNat.XgcdType.IsReduced

added def PNat.XgcdType.IsSpecial'

added def PNat.XgcdType.IsSpecial

modified theorem PNat.XgcdType.finish_isReduced

modified theorem PNat.XgcdType.finish_isSpecial

modified theorem PNat.XgcdType.flip_isReduced

modified theorem PNat.XgcdType.flip_isSpecial

deleted def PNat.XgcdType.isReduced'

deleted def PNat.XgcdType.isReduced

modified theorem PNat.XgcdType.isReduced_iff

deleted def PNat.XgcdType.isSpecial'

deleted def PNat.XgcdType.isSpecial

modified theorem PNat.XgcdType.isSpecial_iff

added theorem PNat.XgcdType.reduce_isReduced'

added theorem PNat.XgcdType.reduce_isReduced

added theorem PNat.XgcdType.reduce_isSpecial'

added theorem PNat.XgcdType.reduce_isSpecial

deleted theorem PNat.XgcdType.reduce_reduced'

deleted theorem PNat.XgcdType.reduce_reduced

deleted theorem PNat.XgcdType.reduce_special'

deleted theorem PNat.XgcdType.reduce_special

modified theorem PNat.XgcdType.start_isSpecial

modified theorem PNat.XgcdType.step_isSpecial