Commit 2025-10-31 08:47 1cd54028

View on Github →

chore: remove declarations deprecated before 2025-04-21 (#30759) I am happy to remove some deprecated declarations for you! Please check if there are any remaining stray comments or other issues before merging. The following files contained only deprecated declarations and have been deleted:

  • Mathlib/Deprecated/AnalyticManifold.lean
  • Mathlib/Geometry/Manifold/AnalyticManifold.lean

Estimated changes

deleted theorem MonoidHom.comp_id_commGrp
deleted theorem MonoidHom.comp_id_grp
deleted theorem MonoidHom.id_commGrp_comp
deleted theorem MonoidHom.id_grp_comp
deleted theorem MonoidHom.comp_id_monCat
deleted theorem MonoidHom.id_monCat_comp
deleted theorem CharP.cast_eq_zero_iff'
deleted def leftMul
deleted def rightMul
deleted theorem Submodule.carrier_inj
deleted structure LinearOrderedField
deleted structure LinearOrderedSemifield
deleted structure LinearOrderedAddCommGroup
deleted structure LinearOrderedCommGroup
deleted structure OrderedAddCommGroup
deleted structure OrderedCommGroup
deleted structure LinearOrderedAddCommMonoid
deleted structure LinearOrderedCommMonoid
deleted structure OrderedAddCommMonoid
deleted structure OrderedCancelAddCommMonoid
deleted structure OrderedCancelCommMonoid
deleted structure OrderedCommMonoid
deleted structure LinearOrderedCommRing
deleted structure LinearOrderedCommSemiring
deleted structure LinearOrderedRing
deleted structure LinearOrderedSemiring
deleted structure OrderedCommRing
deleted structure OrderedCommSemiring
deleted structure OrderedRing
deleted structure OrderedSemiring
deleted structure StrictOrderedCommRing
deleted structure StrictOrderedCommSemiring
deleted structure StrictOrderedRing
deleted structure StrictOrderedSemiring
deleted structure NormedLinearOrderedAddGroup
deleted structure NormedLinearOrderedField
deleted structure NormedLinearOrderedGroup
deleted structure NormedOrderedAddGroup
deleted structure NormedOrderedGroup
deleted structure NormedLatticeAddCommGroup
deleted def Monad.cond
deleted def Monad.filter
deleted def Monad.foldl
deleted def Monad.join
deleted def Monad.mapM'
deleted def Monad.mapM
deleted def Monad.sequence'
deleted def Monad.sequence
deleted def Monad.unlessb
deleted def Monad.whenb
deleted def when
deleted def whenM
deleted theorem Fin.val_one''
deleted theorem Finset.attachFin_eq_fin
deleted theorem Finset.coe_fin
deleted theorem Finset.fin_map
deleted theorem Finset.fin_mono
deleted theorem Finset.fin_subset_fin
deleted theorem Finset.mem_fin
deleted theorem Int.card_fintype_Icc
deleted theorem Int.card_fintype_Ico
deleted theorem Int.card_fintype_Ioc
deleted theorem Int.card_fintype_Ioo
deleted theorem Int.card_fintype_uIcc
deleted theorem List.foldr_eta
deleted theorem Option.bind_congr''
deleted theorem Option.bind_eq_some'
deleted theorem Option.map_bind'
deleted theorem Option.none_bind'
deleted theorem Option.some_bind'
deleted def Tree.ofRBNode
deleted def analyticGroupoid
deleted theorem analyticGroupoid_prod
deleted def analyticPregroupoid
deleted theorem mem_analyticGroupoid
deleted theorem Con.mul_ker_mk_eq
deleted theorem ltByCases_comm
deleted theorem ltByCases_congr
deleted theorem ltByCases_eq
deleted theorem ltByCases_eq_iff
deleted theorem ltByCases_gt
deleted theorem ltByCases_lt
deleted theorem ltByCases_ne
deleted theorem ltByCases_not_gt
deleted theorem ltByCases_not_lt
deleted theorem ltByCases_rec
deleted theorem ltTrichotomy_comm
deleted theorem ltTrichotomy_congr
deleted theorem ltTrichotomy_eq
deleted theorem ltTrichotomy_eq_iff
deleted theorem ltTrichotomy_gt
deleted theorem ltTrichotomy_lt
deleted theorem ltTrichotomy_ne
deleted theorem ltTrichotomy_not_gt
deleted theorem ltTrichotomy_not_lt
deleted theorem ltTrichotomy_self
deleted def ltByCases
deleted theorem Fin.Icc_eq_finset_subtype
deleted theorem Fin.Ici_eq_finset_subtype
deleted theorem Fin.Ico_eq_finset_subtype
deleted theorem Fin.Iic_eq_finset_subtype
deleted theorem Fin.Iio_eq_finset_subtype
deleted theorem Fin.Ioc_eq_finset_subtype
deleted theorem Fin.Ioi_eq_finset_subtype
deleted theorem Fin.Ioo_eq_finset_subtype
deleted theorem Fin.card_fintypeIcc
deleted theorem Fin.card_fintypeIci
deleted theorem Fin.card_fintypeIco
deleted theorem Fin.card_fintypeIic
deleted theorem Fin.card_fintypeIio
deleted theorem Fin.card_fintypeIoc
deleted theorem Fin.card_fintypeIoi
deleted theorem Fin.card_fintypeIoo
deleted theorem Fin.card_fintype_uIcc
deleted theorem Nat.card_fintypeIcc
deleted theorem Nat.card_fintypeIco
deleted theorem Nat.card_fintypeIic
deleted theorem Nat.card_fintypeIio
deleted theorem Nat.card_fintypeIoc
deleted theorem Nat.card_fintypeIoo
deleted theorem Set.Ioc_disjoint_Ioc_same
deleted theorem Ordinal.lt_nmul_iff₃'
deleted theorem Ordinal.nmul_def
deleted theorem Ordinal.nmul_nadd_le₃'
deleted def Simps.Config.asFn
deleted theorem TopCat.hom_apply
added theorem isSymmetricRel_idRel
added theorem isSymmetricRel_univ