Commit 2023-01-03 22:15 31a56f75

View on Github →

chore: fix more casing errors per naming scheme (#1232) I've avoided anything under Tactic or test. In correcting the names, I found Option.isNone_iff_eq_none duplicated between Std and Mathlib, so the Mathlib one has been removed.

Estimated changes

added theorem uniq_inv_of_isField
deleted theorem uniq_inv_of_is_field
deleted theorem NoZeroDivisors.toIsDomain
deleted theorem Vieta_formula_quadratic
modified def Fin2.ofNat'
added theorem Part.none_toOption
deleted theorem Part.none_to_option
added theorem Part.some_toOption
deleted theorem Part.some_to_option
added theorem Sum.swap_leftInverse
deleted theorem Sum.swap_left_inverse
added theorem Sum.swap_rightInverse
deleted theorem Sum.swap_right_inverse
added theorem compl_eq_iff_isCompl
deleted theorem compl_eq_iff_is_compl
added theorem eq_compl_iff_isCompl
deleted theorem eq_compl_iff_is_compl
added theorem isBot_iff_isMin
deleted theorem isBot_iff_is_min
added theorem isTop_iff_isMax
deleted theorem isTop_iff_is_max
added theorem InitialSeg.leLT_apply
deleted theorem InitialSeg.leLt_apply
deleted theorem PrincipalSeg.equivLt_top
added theorem PrincipalSeg.topLTTop
deleted theorem PrincipalSeg.topLtTop
added theorem WellFoundedGT.apply
added theorem WellFoundedGT.fix_eq
added def WellFoundedGT
deleted theorem WellFoundedGt.apply
deleted def WellFoundedGt.fix
deleted theorem WellFoundedGt.fix_eq
deleted theorem WellFoundedGt.induction
deleted def WellFoundedGt
added theorem WellFoundedLT.apply
added theorem WellFoundedLT.fix_eq
added def WellFoundedLT
deleted theorem WellFoundedLt.apply
deleted def WellFoundedLt.fix
deleted theorem WellFoundedLt.fix_eq
deleted theorem WellFoundedLt.induction
deleted def WellFoundedLt
added theorem wellFoundedGT_dual_iff
deleted theorem wellFoundedGt_dual_iff
added theorem wellFoundedLT_dual_iff
deleted theorem wellFoundedLt_dual_iff