Commit 2023-08-10 19:52 32de3f67

View on Github →

chore: banish Type _ and Sort _ (#6499) We remove all possible occurences of Type _ and Sort _ in favor of Type* and Sort*. This has nice performance benefits.

Estimated changes

modified theorem AddTorsor.subsingleton_iff
modified theorem vsub_eq_sub
modified theorem Algebra.algebra_ext
modified def Algebra.cast
modified theorem NoZeroSMulDivisors.trans
modified theorem algebraMap.coe_prod
modified theorem algebraMap.coe_sum
modified theorem intCast_smul
modified theorem smul_algebraMap
modified def AlgEquiv.arrowCongr
modified theorem AlgEquiv.arrowCongr_comp
modified theorem AlgEquiv.arrowCongr_symm
modified theorem AlgEquiv.arrowCongr_trans
modified theorem AlgEquiv.map_finsupp_sum
modified theorem AlgEquiv.map_sum
modified def AlgHomClass.toAlgHom
modified theorem NonUnitalAlgebra.coe_iInf
modified theorem NonUnitalAlgebra.mem_iInf
modified theorem Set.smul_mem_center
modified theorem Submodule.prod_span
modified def AlgEquiv.piCongrRight
modified theorem AlgEquiv.piCongrRight_refl
modified theorem AlgEquiv.piCongrRight_symm
modified theorem AlgEquiv.piCongrRight_trans
modified def RestrictScalars
modified theorem AlgEquiv.spectrum_eq
modified theorem Algebra.coe_iInf
modified theorem Algebra.iInf_toSubmodule
modified theorem Algebra.mem_iInf
modified theorem Algebra.toSubring_eq_top
modified theorem Algebra.top_toSubring
modified theorem Subalgebra.algebraMap_eq
modified theorem Subalgebra.center_eq_top
modified theorem Subalgebra.center_toSubring
modified theorem Subalgebra.range_algebraMap
modified theorem algebraMap_mem
modified theorem Subalgebra.mul_toSubmodule
modified theorem Unitization.algHom_ext''
modified theorem Unitization.algHom_ext
modified def Unitization
modified theorem associated_mul_unit_left
modified theorem associated_mul_unit_right
modified theorem associated_unit_mul_left
modified theorem associated_unit_mul_right
modified theorem prime_dvd_prime_iff_eq
modified theorem prime_pow_succ_dvd_mul
modified theorem Finset.card_sigma
modified theorem Finset.eq_prod_range_div'
modified theorem Finset.eq_prod_range_div
modified theorem Finset.prod_congr_set
modified theorem Finset.prod_induction
modified theorem Finset.prod_list_map_count
modified theorem Finset.prod_pi_mulSingle
modified theorem Finset.prod_range_div'
modified theorem Finset.prod_range_div
modified theorem Finset.prod_sigma'
modified theorem Finset.prod_sigma
modified theorem Finset.prod_unique_nonempty
modified theorem Fintype.prod_bijective
modified theorem Fintype.prod_empty
modified theorem Fintype.prod_equiv
modified theorem Fintype.prod_subsingleton
modified theorem Fintype.prod_unique
modified theorem Int.cast_multiset_prod
modified theorem Int.cast_prod
modified theorem List.prod_toFinset
modified theorem Multiset.prod_sum
modified theorem Multiset.sup_powerset_len
modified theorem Units.coe_prod
modified theorem map_prod
modified theorem nat_abs_sum_le
modified theorem Fin.partialProd_left_inv
modified theorem Fin.partialProd_right_inv
modified theorem Fin.prod_Ioi_succ
modified theorem Fin.prod_Ioi_zero
modified theorem Fin.prod_congr'
modified theorem Fin.prod_trunc
modified theorem Fin.prod_univ_add
modified theorem Fin.sum_pow_mul_eq_add_pow
modified theorem finprod_cond_nonneg
modified theorem finprod_curry₃
modified theorem finprod_eq_zero
modified theorem finprod_nonneg
modified theorem finsum_mul
modified theorem finsum_smul'
modified theorem finsum_smul
modified theorem mul_finsum
modified theorem one_le_finprod'
modified theorem one_lt_finprod'
modified theorem single_le_finprod
modified theorem smul_finsum'
modified theorem smul_finsum
modified theorem Finsupp.sum_ite_self_eq'
modified theorem Finsupp.sum_ite_self_eq
modified theorem Finsupp.sum_ite_self_eq_aux
modified theorem map_finsupp_prod
modified theorem Finset.prod_Ico_eq_div
modified theorem Finset.prod_Ico_eq_mul_inv
modified theorem Finset.sum_Ico_Ico_comm
modified theorem Finset.sum_Ico_reflect
modified theorem Finset.sum_range_reflect
modified theorem Multiset.prod_hom'
modified theorem Multiset.prod_hom
modified theorem map_multiset_prod
modified theorem Finset.abs_prod
modified theorem Finset.abs_sum_le_sum_abs
modified theorem Finset.abs_sum_of_nonneg'
modified theorem Finset.abs_sum_of_nonneg
modified theorem Finset.prod_apply
modified theorem Finset.prod_fn
modified theorem Fintype.prod_apply
modified theorem MonoidHom.functions_ext'
modified theorem MonoidHom.functions_ext
modified theorem Pi.list_prod_apply
modified theorem Pi.multiset_prod_apply
modified theorem RingHom.functions_ext
modified theorem prod_mk_prod
modified theorem Finset.prod_add_ordered
modified theorem Finset.prod_one_sub_ordered
modified theorem Finset.prod_sub_ordered
modified theorem Finset.prod_sum
modified theorem Finset.sum_mul_sum
modified theorem BoolRingCat.coe_of
modified def BoolRingCat.of
modified def GroupWithZeroCat.of
modified def CategoryTheory.Free
modified theorem simple_of_finrank_eq_one
modified theorem MonCat.mul_of
modified theorem MonCat.one_of
modified theorem IsLocalization.epi
modified theorem CharP.charP_to_charZero
modified theorem RingHom.charP_iff_charP
modified theorem isSquare_of_charTwo'
modified theorem sum_pow_char
modified theorem isUnit_iff_not_dvd_char
modified theorem prime_dvd_char_iff_dvd_card
modified theorem charP_zero_or_prime_power
modified theorem CharP.quotient'
modified theorem Nat.cast_div_charZero
modified theorem Nat.cast_pow_eq_one
modified def Cubic.disc
modified structure Cubic
modified def DirectSum.IsInternal
modified theorem DirectSum.addHom_ext'
modified theorem DirectSum.addHom_ext
modified theorem DirectSum.coe_of_apply
modified theorem map_dvd
modified theorem Rat.smul_one_eq_coe
modified def FreeAlgebra.liftFun
modified def FreeMonoid.casesOn
modified theorem FreeMonoid.casesOn_of_mul
modified theorem FreeMonoid.casesOn_one
modified def FreeMonoid.recOn
modified theorem FreeMonoid.recOn_of_mul
modified theorem FreeMonoid.recOn_one
modified theorem extract_gcd
modified theorem gcd_greatest
modified theorem gcd_greatest_associated
modified theorem isUnit_gcd_of_eq_mul_gcd
modified theorem Finset.Int.gcd_div_eq_one
modified theorem Finset.Nat.gcd_div_eq_one
modified theorem geom_sum₂_self
modified def GradedMonoid.mk
modified def GradedMonoid
modified theorem SetLike.coe_gMul
modified theorem SetLike.coe_gOne
modified theorem SetLike.coe_gnpow
modified theorem SetLike.mul_mem_graded
modified theorem SetLike.one_mem_graded
modified theorem SetLike.coe_GSmul
modified theorem commutatorElement_def
modified def Commute
modified def ConjClasses
modified theorem isConj_iff_eq
modified def zpowRec
modified def zsmulRec
modified theorem CancelCommMonoid.ext
modified theorem CancelMonoid.ext
modified theorem CommGroup.ext
modified theorem CommMonoid.ext
modified theorem DivInvMonoid.ext
modified theorem Group.ext
modified def MonoidHom.toOpposite
modified def MulEquiv.inv'
modified def MulHom.fromOpposite
modified def MulHom.toOpposite
modified def MonoidHom.coeFn
modified def MulHom.coeFn
modified def Pi.constMonoidHom
modified def Pi.constMulHom
modified theorem Set.preimage_one
modified theorem MonoidHom.comp_coprod
modified theorem MonoidHom.coprod_inl_inr
modified theorem MulHom.comp_coprod
modified def Units.embedProduct
modified def Additive
modified def Multiplicative
modified theorem ofAdd_eq_one
modified theorem ofMul_eq_zero
modified theorem Units.isUnit_units_mul
modified theorem Units.val_inv_eq_inv_val
modified theorem unique_one
modified def WithOne.recOneCoe
modified theorem pow_eq_pow_mod
modified theorem map_zpow₀
modified theorem MonoidWithZero.coe_inverse
modified theorem Units.smul_mk0
modified def invMonoidWithZeroHom
modified def MulAut
modified structure CentroidHom
modified def mulLeftEmbedding
modified def mulRightEmbedding
modified structure AddEquiv
modified def MonoidHom.inverse
modified def MulEquiv.arrowCongr
modified theorem MulEquiv.comp_symm_eq
modified theorem MulEquiv.eq_comp_symm
modified theorem MulEquiv.eq_symm_comp
modified def MulEquiv.piCongrRight
modified theorem MulEquiv.piCongrRight_refl
modified theorem MulEquiv.piCongrRight_symm
modified theorem MulEquiv.piCongrRight_trans
modified def MulEquiv.refl
modified def MulEquiv.symm
modified theorem MulEquiv.symm_comp_eq
modified structure MulEquiv
modified def MulEquiv.inv
modified theorem MulEquiv.inv_symm
modified structure AddFreimanHom
modified structure FreimanHom
modified structure AddHom
modified structure AddMonoidHom
modified theorem MonoidHom.coe_of_map_div
modified theorem MonoidHom.comp_assoc
modified def MonoidHom.id
modified def MonoidHom.ofMapDiv
modified def MonoidHom.ofMapMulInv
modified structure MonoidHom
modified def MonoidWithZeroHom.id
modified structure MonoidWithZeroHom
modified theorem MulHom.comp_assoc
modified def MulHom.id
modified structure MulHom
modified theorem OneHom.comp_assoc
modified def OneHom.id
modified structure OneHom
modified structure ZeroHom
modified theorem map_ne_one_iff
modified theorem ne_one_of_map
modified theorem hom_coe_pow
modified structure NonUnitalRingHom
modified theorem RingHom.coe_coe
modified def RingHom.id
modified theorem RingHom.map_ite_one_zero
modified theorem RingHom.map_ite_zero_one
modified structure RingHom
modified theorem MonoidHom.coe_toHomUnits
modified def MonoidHom.toHomUnits
modified theorem map_units_inv
modified def ComplexShape.down'
modified theorem ComplexShape.down'_mk
modified def ComplexShape.down
modified theorem ComplexShape.down_mk
modified def ComplexShape.refl
modified def ComplexShape.up'
modified def ComplexShape.up
modified structure ComplexShape
modified theorem ChainComplex.next
modified theorem ChainComplex.prev
modified theorem CochainComplex.next
modified theorem CochainComplex.prev
modified def HomotopyEquiv.ofIso
modified theorem CategoryTheory.Split.map
modified theorem MonoidHom.map_mulIndicator
modified theorem Set.indicator_diff
modified theorem Set.mulIndicator_range_comp
modified def Invertible.map
modified theorem commute_invOf
modified theorem map_invOf
modified structure LieHom
modified theorem LieRing.lie_apply
modified structure LinearRecurrence
modified theorem Int.smul_one_eq_coe
modified theorem Module.ext'
modified theorem Nat.smul_one_eq_coe
modified theorem inv_int_cast_smul_comm
modified theorem inv_int_cast_smul_eq
modified theorem inv_nat_cast_smul_comm
modified theorem inv_nat_cast_smul_eq
modified theorem map_int_cast_smul
modified theorem map_inv_int_cast_smul
modified theorem map_inv_nat_cast_smul
modified theorem map_nat_cast_smul
modified theorem map_rat_cast_smul
modified theorem map_rat_smul
modified theorem rat_cast_smul_eq
modified theorem smul_add_one_sub_smul
modified theorem LinearEquiv.comp_symm_eq
modified theorem LinearEquiv.eq_comp_symm
modified theorem LinearEquiv.eq_symm_comp
modified theorem LinearEquiv.symm_comp_eq
modified structure LinearEquiv
modified theorem LinearMap.map_smul_of_tower
modified structure LinearMap
modified theorem IsLocalizedModule.mk'_neg
modified theorem IsLocalizedModule.mk'_sub
modified theorem LocalizedModule.liftOn_mk
modified theorem LocalizedModule.mk_mul_mk
modified theorem LocalizedModule.mk_neg
modified theorem IsSMulRegular.pi
modified theorem Module.Projective.of_basis
modified theorem Submodule.mem_iSup_of_mem
modified theorem Submodule.sub_mem_sup
modified theorem Submodule.sum_mem_biSup
modified theorem Submodule.sum_mem_iSup
modified theorem Submodule.neg_iInf
modified theorem Submodule.neg_iSup
modified def Module.IsTorsion'
modified theorem AddMonoidAlgebra.liftNC_mul
modified theorem AddMonoidAlgebra.liftNC_one
modified theorem MonoidAlgebra.liftNC_mul
modified theorem MonoidAlgebra.liftNC_one
modified theorem MonoidAlgebra.liftNC_smul
modified theorem MonoidAlgebra.mapDomain_mul
modified theorem MonoidAlgebra.mapDomain_one
modified theorem MonoidAlgebra.mapDomain_sum
modified theorem neZero_iff
modified theorem not_neZero
modified theorem MulOpposite.op_smul
modified theorem MulOpposite.unop_smul
modified structure AbsoluteValue
modified theorem Monotone.div_const
modified theorem StrictMono.div_const
modified theorem Nat.ceil_intCast
modified theorem apply_abs_le_mul_of_one_le'
modified theorem apply_abs_le_mul_of_one_le
modified structure AddCommGroup.PositiveCone
modified structure AddCommGroup.TotalPositiveCone
modified theorem div_le_div_flip
modified structure OrderAddMonoidHom
modified structure OrderMonoidHom
modified structure OrderMonoidWithZeroHom
modified structure OrderRingHom
modified structure OrderRingIso
modified theorem pos_of_gt
modified theorem Mul.to_covariantClass_left
modified theorem Mul.to_covariantClass_right
modified theorem cmp_mul_left'
modified theorem cmp_mul_right'
modified structure Ring.PositiveCone
modified structure Ring.TotalPositiveCone
modified theorem OrderIso.map_tsub
modified theorem le_mul_tsub
modified theorem le_tsub_mul
modified theorem PUnit.smul_eq
modified theorem range_two_mul_add_one
modified theorem Finset.periodic_prod
modified def Quandle.Conj.map
modified def Quandle.Conj
modified theorem Quandle.conj_act_eq_conj
modified theorem Quandle.conj_swap
modified def Rack.EnvelGroup
modified def Rack.IsAbelian
modified def Rack.IsInvolutory
modified theorem Rack.ad_conj
modified theorem Rack.assoc_iff_id
modified def Rack.envelAction
modified theorem Rack.envelAction_prop
modified def Rack.selfApplyEquiv
modified def Rack.toConj
modified def Rack.toEnvelGroup.map
modified theorem Rack.toEnvelGroup.univ
modified theorem Rack.toEnvelGroup.univ_uniq
modified def Rack.toEnvelGroup
modified def ShelfHom.id
modified structure ShelfHom
modified def Quaternion.equivProd
modified def Quaternion.equivTuple
modified theorem Quaternion.equivTuple_apply
modified def Quaternion
modified theorem QuaternionAlgebra.mk.eta
modified structure QuaternionAlgebra
modified structure QuaternionAlgebra.Basis
modified structure IsAddRegular
modified def RingAut
modified def AsBoolAlg
modified def AsBoolRing
modified theorem ite_and_mul_zero
modified theorem ite_mul_zero_left
modified theorem ite_mul_zero_right
modified def AddEquiv.toRingEquiv
modified def MulEquiv.toRingEquiv
modified def RingEquiv.ofHomInv'
modified def RingEquiv.ofHomInv
modified theorem RingEquiv.piCongrRight_refl
modified theorem RingEquiv.piCongrRight_symm
modified structure RingEquiv
modified def RingEquiv.piFinTwo
modified def RingHom.fromOpposite
modified def RingHom.toOpposite
modified def Pi.constRingHom
modified def smulMonoidWithZeroHom
modified theorem RingHom.star_apply
modified theorem RingHom.star_def
modified def starRingOfComm
modified def starSemigroupOfComm
modified theorem star_id_of_comm
modified theorem star_invOf
modified theorem star_prod
modified theorem star_sum
modified theorem algebraMap_star_comm
modified def starLinearEquiv
modified theorem star_rat_smul
modified theorem Function.star_sum_elim
modified theorem Set.iInter_star
modified theorem Set.iUnion_star
modified theorem Set.star_singleton
modified theorem StarMemClass.star_coe_eq
modified theorem IsSelfAdjoint.starHom_apply
modified theorem isSelfAdjoint_starHom_apply
modified structure NonUnitalStarAlgHom
modified structure StarAlgEquiv
modified structure StarAlgHom
modified theorem StarSubalgebra.coe_iInf
modified theorem StarSubalgebra.mem_iInf
modified def unitary
modified theorem SymAlg.sym_smul
modified theorem SymAlg.unsym_smul
modified def SymAlg
modified theorem Tropical.mul_eq_zero_iff
modified theorem Tropical.trop_smul
modified theorem Tropical.untrop_pow
modified theorem simply_connected_def
modified theorem Asymptotics.isBigOWith_pi
modified theorem Asymptotics.isBigO_pi
modified theorem Asymptotics.isLittleO_pi
modified theorem Filter.Tendsto.cesaro_smul
modified theorem BoundedVariationOn.dist_le
modified theorem BoxIntegral.HasIntegral.sum
modified structure BoxIntegral.Box
modified structure BoxIntegral.BoxAdditiveMap
modified structure ContDiffBumpBase
modified def someContDiffBumpBase
modified theorem ContDiff.sum
modified theorem ContDiffAt.sum
modified theorem ContDiffOn.prod_map
modified theorem ContDiffOn.sum
modified theorem ContDiffWithinAt.sum
modified theorem derivWithin_Ioi_eq_Ici
modified theorem DiffContOnCl.const_smul
modified theorem DiffContOnCl.smul
modified theorem DiffContOnCl.smul_const
modified theorem HasFDerivAt.lim
modified theorem HasFDerivWithinAt.lim
modified structure ImplicitFunctionData
modified theorem UniqueDiffOn.pi
modified theorem UniqueDiffOn.univ_pi
modified theorem UniqueDiffWithinAt.pi
modified theorem UniqueDiffWithinAt.univ_pi
modified theorem mapsTo_tangentCone_pi
modified theorem tangentConeAt.lim_zero
modified theorem Directed.convex_iUnion
modified theorem convex_iInter
modified theorem convex_iInter₂
modified theorem convex_pi
modified structure ConvexBody
modified theorem Convex.finsum_mem
modified theorem ConvexCone.coe_iInf
modified theorem ConvexCone.mem_iInf
modified theorem innerDualCone_iUnion
modified structure ProperCone
modified theorem isExtreme_iInter
modified theorem starConvex_iInter
modified theorem starConvex_iUnion
modified theorem starConvex_pi
modified theorem hofer
modified theorem pos_div_pow_pos
modified theorem DFinsupp.inner_sum
modified theorem DFinsupp.sum_inner
modified theorem Finsupp.inner_sum
modified theorem Finsupp.sum_inner
modified structure InnerProductSpace.Core
modified theorem OrthogonalFamily.comp
modified def OrthogonalFamily
modified theorem Orthonormal.codRestrict
modified theorem Orthonormal.comp
modified theorem Orthonormal.equiv_apply
modified theorem inner_sum
modified theorem orthonormal_span
modified theorem sum_inner
modified theorem gramSchmidt_zero
modified theorem Orientation.volumeForm_map
modified theorem Submodule.iInf_orthogonal
modified theorem Submodule.isOrtho_iSup_left
modified theorem EuclideanSpace.dist_eq
modified theorem EuclideanSpace.edist_eq
modified theorem EuclideanSpace.nndist_eq
modified theorem EuclideanSpace.nnnorm_eq
modified theorem EuclideanSpace.norm_eq
modified def EuclideanSpace
modified theorem PiLp.inner_apply
modified theorem reflection_map
modified theorem reflection_map_apply
modified theorem Orientation.areaForm_map
modified theorem Orientation.kahler_map
modified theorem Set.Finite.absorbs_iUnion
modified theorem absorbs_iUnion_finset
modified theorem Seminorm.const_isBounded
modified theorem Seminorm.isBounded_const
modified theorem withSeminorms_iInf
modified theorem MellinConvergent.const_smul
modified theorem mellin_const_smul
modified theorem Finset.nnnorm_prod_le'
modified theorem Finset.nnnorm_prod_le
modified theorem Finset.norm_prod_le'
modified theorem Finset.norm_prod_le
modified theorem NormOneClass.induced
modified theorem NormOneClass.nontrivial
modified def Submonoid.unitSphere
modified def Subsemigroup.unitBall
modified def unitSphereToUnits
modified theorem NormedAddGroupHom.coe_sum
modified theorem NormedAddGroupHom.norm_id
modified theorem NormedAddGroupHom.sum_apply
modified structure NormedAddGroupHom
modified theorem exists_pos_bound_of_bound
modified theorem NormedAddGroupHom.lift_mk
modified structure AddGroupNorm
modified structure AddGroupSeminorm
modified structure GroupNorm
modified structure GroupSeminorm
modified structure NonarchAddGroupNorm
modified structure NonarchAddGroupSeminorm
modified structure MulRingNorm
modified structure MulRingSeminorm
modified structure RingNorm
modified structure RingSeminorm
modified def normRingNorm
modified def normRingSeminorm
modified theorem AffineMap.isOpenMap
modified theorem banach_steinhaus
modified def NormedAlgebra.induced
modified def NormedSpace.induced
modified structure IsBoundedLinearMap
modified theorem isBoundedBilinearMap_smul
modified theorem IsCompactOperator.smul
modified def IsCompactOperator
modified theorem isCompactOperator_zero
modified def IsConformalMap
modified def NormedSpace.polar
modified structure ENorm
modified theorem Function.update_exp
modified theorem Pi.exp_apply
modified theorem Pi.exp_def
modified theorem Basis.exists_op_nnnorm_le
modified theorem Basis.exists_op_norm_le
modified theorem Basis.op_nnnorm_le
modified theorem Basis.op_norm_le
modified theorem IsEquivalent.summable_iff
modified theorem continuousOn_clm_apply
modified theorem continuous_clm_apply
modified theorem summable_norm_iff
modified theorem summable_of_isBigO'
modified theorem summable_of_isBigO_nat'
modified theorem summable_of_isEquivalent
modified theorem Basis.ext_linearIsometry
modified structure LinearIsometry
modified theorem PiLp.dist_eq_of_L2
modified theorem PiLp.edist_eq_of_L2
modified theorem PiLp.iSup_edist_ne_top_aux
modified theorem PiLp.nndist_eq_iSup
modified theorem PiLp.nndist_eq_of_L2
modified theorem PiLp.nndist_eq_sum
modified theorem PiLp.nnnorm_eq_ciSup
modified theorem PiLp.nnnorm_eq_of_L2
modified theorem PiLp.nnnorm_eq_sum
modified theorem PiLp.norm_eq_of_L2
modified theorem PiLp.norm_eq_of_nat
modified theorem PiLp.norm_sq_eq_of_L2
modified def PiLp
modified def PreLp
modified theorem lp.coeFn_sum
modified def lp
modified theorem IsPicardLindelof.norm_le₀
modified structure IsPicardLindelof
modified structure PicardLindelof
modified structure Seminorm
modified theorem Filter.Tendsto.arsinh
modified theorem StrictConcaveOn.add_const
modified theorem StrictConvexOn.add_const
modified theorem Real.logb_prod
modified theorem Real.log_prod
modified theorem Filter.Tendsto.nnrpow
modified theorem Real.exists_rat_pow_btwn
modified theorem Real.rpow_sum_of_nonneg
modified theorem Real.rpow_sum_of_pos
modified theorem tendsto_nat_floor_atTop
modified theorem tendsto_norm_zero'
modified theorem Bipointed.coe_of
modified def Bipointed.of
modified def PartialFun.of
modified theorem Pointed.coe_of
modified def Pointed.of
modified theorem TwoP.coe_of
modified def TwoP.of
modified theorem CategoryTheory.dcongr_arg
modified def FintypeCat.incl
modified def FintypeCat.of
modified theorem CategoryTheory.sum_tensor
modified theorem CategoryTheory.tensor_sum
modified theorem CategoryTheory.op_sum
modified theorem CategoryTheory.unop_sum
modified theorem Finset.card_add_nsmul_le
modified theorem mulSalemSpencer_pi
modified theorem Colex.hom_le_iff
modified theorem Colex.hom_lt_iff
modified def derangements
modified theorem card_derangements_invariant
modified structure Combinatorics.Line.AlmostMono
modified structure Combinatorics.Line
modified def Prefunctor.comp
modified theorem Prefunctor.comp_assoc
modified theorem Prefunctor.comp_id
modified def Prefunctor.id
modified theorem Prefunctor.id_comp
modified def Quiver.SingleObj
modified def Quiver.Labelling
modified def Quiver.Symmetrify
modified theorem Finpartition.coe_energy
modified def Turing.EvalsTo.refl
modified def Turing.EvalsTo.trans
modified structure Turing.EvalsTo
modified structure Turing.EvalsToInTime
modified theorem Turing.TM2to1.stk_nth_val
modified structure Turing.Tape
modified def Turing.evalInduction
modified def Turing.proj
modified theorem Turing.proj_map_nth
modified def Functor.AddConst
modified def Functor.Const
modified structure CFilter
modified theorem Ctop.Realizer.ext'
modified theorem Ctop.Realizer.ext
modified structure Ctop
modified theorem Bool.injective_iff
modified theorem Bool.range_eq
modified def Bundle.Pullback
modified structure Bundle.TotalSpace
modified def Bundle.Trivial
modified theorem Complex.abs_prod
modified theorem Complex.exp_sum
modified theorem Real.exp_sum
modified theorem abv_sum_le_sum_abv
modified theorem isCauSeq_geo_series
modified theorem sum_range_diag_flip
modified theorem Complex.coe_smul
modified theorem finrank_real_of_complex
modified theorem rank_real_of_complex
modified theorem Countable.of_equiv
modified theorem DFinsupp.comp_liftAddHom
modified theorem DFinsupp.comp_sumAddHom
modified theorem DFinsupp.prod_comm
modified theorem DFinsupp.smul_sum
modified theorem DFinsupp.sumAddHom_comm
modified theorem dfinsupp_sumAddHom_mem
modified def Std.DList.join
modified theorem Std.DList_lazy
modified theorem Std.DList_singleton
modified def ENat.recTopCoe
modified theorem ENat.recTopCoe_coe
modified theorem ENat.recTopCoe_top
modified theorem Fin.antitone_iff_succ_le
modified def Fin.elim0'
modified theorem Fin.liftFun_iff_succ
modified theorem Fin.monotone_iff_le_succ
modified theorem Fin.strictAnti_iff_succ_lt
modified theorem Fin.strictMono_iff_lt_succ
modified def finZeroElim
modified def Fin.append
modified theorem Fin.append_assoc
modified theorem Fin.append_elim0'
modified theorem Fin.append_left
modified theorem Fin.append_left_eq_cons
modified theorem Fin.append_left_nil
modified theorem Fin.append_right
modified theorem Fin.append_right_eq_snoc
modified theorem Fin.append_right_nil
modified theorem Fin.comp_cons
modified theorem Fin.comp_init
modified theorem Fin.comp_snoc
modified theorem Fin.comp_tail
modified def Fin.consInduction
modified theorem Fin.cons_snoc_eq_snoc_cons
modified theorem Fin.elim0'_append
modified theorem Fin.exists_fin_zero_pi
modified theorem Fin.forall_fin_zero_pi
modified theorem Fin.init_def
modified theorem Fin.range_cons
modified theorem Fin.repeat_add
modified theorem Fin.repeat_apply
modified theorem Fin.repeat_one
modified theorem Fin.repeat_succ
modified theorem Fin.repeat_zero
modified theorem Fin.snoc_cast_add
modified theorem Fin.tail_def
modified theorem Fin.tail_init_eq_init_tail
modified theorem Fin.tuple0_le
modified def Fin.«repeat»
modified theorem Tuple.bubble_sort_induction
modified theorem Matrix.empty_val'
modified def Matrix.vecAppend
modified theorem Matrix.vecAppend_apply_zero
modified theorem Matrix.vecAppend_eq_ite
modified theorem Finite.cast_card_eq_mk
modified def Finite.equivFin
modified theorem Nat.card_eq
modified theorem Finite.exists_equiv_fin
modified theorem Finite.of_equiv
modified theorem finite_iff_exists_equiv_fin
modified theorem finite_or_infinite
modified theorem not_finite
modified theorem Finset.cons_induction
modified theorem Finset.cons_induction_on
modified theorem Finset.induction_on'
modified theorem Finset.pairwiseDisjoint_coe
modified def Finset.piecewise
modified theorem Finset.piecewise_mem_Icc'
modified theorem Finset.piecewise_mem_Icc
modified theorem Finset.piecewise_mem_set_pi
modified theorem Finset.update_eq_piecewise
modified structure Finset
modified theorem Finset.strongInductionOn_eq
modified theorem Finset.strongInduction_eq
modified theorem Finset.fold_disjiUnion
modified theorem Finset.inf'_mem
modified theorem Finset.inf_sup
modified theorem Finset.sup'_mem
modified theorem Finset.sup_inf
modified theorem Finset.sup_sdiff_right
modified theorem Finset.image₂_assoc
modified theorem Finset.image₂_left_comm
modified theorem Finset.image₂_right_comm
modified theorem Finset.noncommProd_eq_prod
modified def Finset.Pi.empty
modified theorem Finset.pi_const_singleton
modified theorem Finset.pi_singletons
modified theorem Finset.coe_prod
modified theorem Finset.powersetLen_map
modified theorem Finset.sigma_preimage_mk
modified theorem Finsupp.coe_sumElim
modified def Finsupp.sumElim
modified theorem Finsupp.sumElim_apply
modified theorem Finsupp.sumElim_inl
modified theorem Finsupp.sumElim_inr
modified structure Finsupp
modified theorem Finsupp.isPwo
modified theorem Finset.piecewise_erase_univ
modified theorem Finset.piecewise_univ
modified theorem Fintype.choose_subtype_eq
modified def Fintype.ofEquiv
modified def Unique.fintype
modified theorem Finset.card_pi
modified theorem Finset.prod_univ_pi
modified theorem Fintype.card_pi
modified theorem Fintype.card_piFinset
modified theorem Finite.of_injective
modified theorem Finite.of_surjective
modified theorem Finset.exists_maximal
modified theorem Finset.exists_minimal
modified theorem Finset.univ_map_embedding
modified theorem Fintype.card_lex
modified theorem Fintype.card_orderDual
modified theorem Fintype.card_plift
modified theorem Fintype.card_range
modified theorem Fintype.card_range_le
modified theorem Fintype.card_ulift
modified theorem List.Nodup.length_le_card
modified theorem Set.toFinset_card
modified theorem finite_iff_nonempty_fintype
modified theorem isEmpty_fintype
modified theorem nonempty_fintype
modified theorem Fintype.card_embedding_eq
modified theorem Fintype.card_option
modified def fintypeOfOption
modified theorem univ_option
modified theorem Directed.fintype_le
modified theorem Fintype.bddAbove_range
modified theorem Fintype.bddBelow_range
modified theorem Fintype.exists_ge
modified theorem Fintype.exists_le
modified theorem Finset.univ_pi_univ
modified theorem Fintype.piFinset_univ
modified theorem Finset.univ_filter_card_eq
modified theorem Finset.univ_product_univ
modified theorem Fintype.card_prod
modified theorem Pi.infinite_of_exists_right
modified def Quotient.finChoice
modified def Quotient.finChoiceAux
modified theorem Quotient.finChoiceAux_eq
modified theorem Quotient.finChoice_eq
modified theorem Finset.univ_sigma_univ
modified def monoEquivOfFin
modified theorem Finset.univ_disjSum_univ
modified structure CoolerHom
modified theorem do_something
modified theorem map_cool
modified theorem map_op
modified structure CoolerEmbedding
modified theorem do_something
modified theorem map_cool
modified theorem map_op
modified structure CoolerIso
modified theorem do_something
modified theorem map_cool
modified def Int.castAddHom
modified def Int.castRingHom
modified theorem RingHom.ext_int
modified theorem Sum.elim_intCast_intCast
modified theorem Int.cast_div_charZero
modified theorem RingHom.injective_int
modified theorem pow_gcd_eq_one
modified theorem Nat.cast_natAbs
modified theorem IsROrC.ofReal_finsupp_prod
modified theorem IsROrC.ofReal_finsupp_sum
modified theorem IsROrC.ofReal_prod
modified theorem IsROrC.ofReal_sum
modified def AList.insertRec
modified theorem AList.insertRec_empty
modified theorem AList.insertRec_insert
modified theorem AList.insertRec_insert_mk
modified def List.bidirectionalRec
modified theorem List.findIdx_nil
modified def List.foldlRecOn
modified theorem List.foldlRecOn_nil
modified def List.foldrRecOn
modified theorem List.foldrRecOn_cons
modified theorem List.foldrRecOn_nil
modified theorem List.getLast_pmap
modified theorem List.injective_foldl_comp
modified theorem List.map_drop
modified theorem List.map_take
modified theorem List.pmap_append'
modified def List.reverseRecOn
modified theorem List.prod_hom
modified theorem List.prod_isUnit_iff
modified theorem List.prod_map_hom
modified theorem List.prod_map_mul
modified theorem map_list_prod
modified theorem unop_map_list_prod
modified theorem Cycle.chain_map
modified def Cycle.map
modified theorem Cycle.map_coe
modified theorem Cycle.map_eq_nil
modified theorem Cycle.map_nil
modified theorem Cycle.mem_map
modified def Cycle
modified def List.alternatingProd
modified def List.alternatingSum
modified theorem List.Func.nil_sub
modified theorem List.Func.sub_nil
modified theorem List.Nodup.sigma
modified theorem List.map_ofFn
modified def List.ofFnRec
modified theorem List.ofFnRec_ofFn
modified theorem List.pairwise_replicate
modified theorem List.Perm.rec_heq
modified theorem List.Perm.take_inter
modified theorem List.Subperm.cons_right
modified theorem List.IsRotated.map
modified def List.IsRotated.setoid
modified theorem List.map_rotate
modified theorem List.zipWith_rotate_distrib
modified theorem List.zipWith_rotate_one
modified theorem List.sizeOf_dedupKeys
modified theorem List.sizeOf_kerase
modified theorem List.length_of_sublistsLen
modified theorem List.length_sublistsLen
modified theorem List.mem_sublistsLen
modified theorem List.mem_sublistsLen_self
modified def List.sublistsLen
modified def List.sublistsLenAux
modified theorem List.sublistsLenAux_append
modified theorem List.sublistsLenAux_eq
modified theorem List.sublistsLenAux_zero
modified theorem List.sublistsLen_succ_cons
modified theorem List.sublistsLen_succ_nil
modified theorem List.sublistsLen_zero
modified theorem List.exists_tfae
modified theorem List.forall_tfae
modified theorem List.toFinsupp_append
modified theorem List.map_zipWith
modified theorem Matrix.conjTranspose_sum
modified theorem Matrix.map_map
modified theorem Matrix.reindex_trans
modified theorem Matrix.submatrix_mul
modified theorem Matrix.submatrix_mul_equiv
modified theorem Matrix.submatrix_smul
modified theorem Matrix.submatrix_submatrix
modified theorem Matrix.transpose_smul
modified theorem Matrix.transpose_sum
modified theorem Matrix.two_mul_expl
modified theorem Matrix.blockDiag'_smul
modified theorem Matrix.blockDiag_smul
modified theorem Matrix.blockDiagonal'_smul
modified theorem Matrix.blockDiagonal_smul
modified theorem Matrix.toBlock_mul_eq_add
modified theorem Matrix.toBlock_mul_eq_mul
modified theorem Matrix.kroneckerMap_assoc
modified theorem Matrix.smul_mat_empty
modified theorem Matrix.smul_vec2
modified theorem Matrix.smul_vec3
modified theorem Multiset.antidiagonal_zero
modified theorem Multiset.count_map
modified theorem Multiset.le_bind
modified theorem Multiset.map_univ
modified theorem Multiset.prod_toEnumFinset
modified theorem Multiset.fold_bind
modified theorem Multiset.id_traverse
modified theorem Multiset.lift_coe
modified theorem Multiset.map_traverse
modified theorem Multiset.traverse_map
modified theorem Multiset.nodup_sup_iff
modified def Multiset.Pi.empty
modified theorem Multiset.bind_powerset_len
modified theorem Multiset.powersetLen_empty
modified theorem Multiset.powersetLen_map
modified theorem MvPolynomial.C_inj
modified theorem MvPolynomial.C_injective
modified theorem MvPolynomial.C_surjective
modified theorem MvPolynomial.aeval_prod
modified theorem MvPolynomial.aeval_sum
modified theorem MvPolynomial.algHom_ext'
modified theorem MvPolynomial.algHom_ext
modified theorem MvPolynomial.coeff_smul
modified theorem MvPolynomial.coeff_sum
modified theorem MvPolynomial.comp_aeval
modified theorem MvPolynomial.eval_prod
modified theorem MvPolynomial.eval_sum
modified theorem MvPolynomial.linearMap_ext
modified theorem MvPolynomial.map_aeval
modified theorem MvPolynomial.ringHom_ext'
modified theorem MvPolynomial.ringHom_ext
modified theorem MvPolynomial.smul_monomial
modified theorem MvPolynomial.sum_C
modified theorem MvPolynomial.support_smul
modified theorem MvPolynomial.support_sum
modified def MvPolynomial
modified theorem MvPolynomial.funext
modified theorem MvPolynomial.funext_iff
modified theorem MvPolynomial.bind₁_rename
modified theorem MvPolynomial.rename_bind₁
modified theorem MvPolynomial.degrees_prod
modified theorem MvPolynomial.degrees_sum
modified theorem MvPolynomial.vars_prod
modified def Nat.leRecOn'
modified def Nat.pincerRecursion
modified def Nat.strongRecOn'
modified theorem Nat.strongRecOn'_beta
modified def Nat.binaryRec'
modified def Nat.binaryRecFromOne
modified theorem Nat.binaryRec_eq'
modified def Nat.castAddMonoidHom
modified def Nat.castRingHom
modified theorem Sum.elim_natCast_natCast
modified theorem Finset.prod_pow_choose_succ
modified theorem Nat.coe_ofDigits
modified def Nat.ofDigits
modified theorem Nat.ofDigits_eq_foldr
modified theorem Nat.ofDigits_one_cons
modified def Nat.evenOddRec
modified theorem Nat.evenOddRec_even
modified theorem Nat.evenOddRec_odd
modified theorem Nat.evenOddRec_zero
modified theorem Nat.factorization_prod
modified def Nat.recOnPrimeCoprime
modified def Nat.recOnPrimePow
modified theorem Nat.coprime_prod_left
modified theorem Nat.coprime_prod_right
modified theorem Nat.iInf_of_empty
modified theorem Nat.range_casesOn
modified theorem Nat.range_rec
modified def NzsNum.drec'
modified def SNum.drec'
modified theorem Option.choice_eq_none
modified theorem Option.some_injective
modified theorem Option.elim'_eq_elim
modified theorem Option.mem_some_iff
modified def Ordset
modified theorem PFun.coe_id
modified def PFun.fixInduction'
modified theorem PFun.fixInduction'_fwd
modified theorem PFun.fixInduction'_stop
modified def PFun.fixInduction
modified theorem PFun.fixInduction_spec
modified def PFun
modified def MvPFunctor.wRec
modified theorem MvPFunctor.wRec_eq
modified def MvPFunctor.wpRec
modified theorem MvPFunctor.wpRec_eq
modified def PFunctor.Obj
modified def PFunctor.map
modified theorem PFunctor.M.bisim'
modified theorem PFunctor.M.casesOn_mk'
modified theorem PFunctor.M.casesOn_mk
modified theorem PFunctor.M.cases_mk
modified def PFunctor.M.corecOn
modified def PNat.recOn
modified theorem PNat.recOn_succ
modified theorem Part.elim_toOption
modified theorem Pi.mulSingle_op
modified theorem Pi.mulSingle_op₂
modified def uniqueOfSurjectiveOne
modified theorem Polynomial.aeval_comp
modified theorem Polynomial.aeval_fn_apply
modified theorem IsSMulRegular.polynomial
modified theorem Polynomial.addHom_ext'
modified theorem Polynomial.addHom_ext
modified theorem Polynomial.lhom_ext'
modified theorem Polynomial.ofFinsupp_smul
modified theorem Polynomial.ofFinsupp_sum
modified def Polynomial.sum
modified theorem Polynomial.sum_X_index
modified theorem Polynomial.sum_add'
modified theorem Polynomial.sum_add
modified theorem Polynomial.sum_add_index
modified theorem Polynomial.sum_def
modified theorem Polynomial.sum_eq_of_subset
modified theorem Polynomial.sum_smul_index
modified theorem Polynomial.sum_zero_index
modified theorem Polynomial.toFinsupp_smul
modified theorem Polynomial.toFinsupp_sum
modified structure Polynomial
modified theorem Polynomial.finset_sum_coeff
modified theorem Polynomial.int_cast_inj
modified def Polynomial.lsum
modified theorem Polynomial.nat_cast_inj
modified theorem Polynomial.Monic.ne_zero
modified theorem one_le_pow_mul_abs_eval_div
modified theorem Polynomial.derivative_smul
modified theorem Polynomial.IsRoot.dvd
modified theorem Polynomial.comp_assoc
modified theorem Polynomial.eval_prod
modified theorem Polynomial.eval₂_at_apply
modified theorem Polynomial.eval₂_at_one
modified theorem Polynomial.eval₂_congr
modified theorem Polynomial.isRoot_map_iff
modified theorem Polynomial.isRoot_prod
modified def Polynomial.leval
modified theorem Polynomial.mem_map_range
modified theorem Polynomial.mul_comp
modified theorem Polynomial.pow_comp
modified theorem Polynomial.prod_comp
modified theorem Polynomial.expand_aeval
modified theorem Polynomial.rootSet_prod
modified def PolynomialModule
modified theorem Polynomial.Monic.isRegular
modified theorem div_eq_quo_add_sum_rem_div
modified theorem Polynomial.mem_rootSet'
modified theorem Polynomial.mem_rootSet
modified theorem Polynomial.rootSet_finite
modified theorem Polynomial.roots_prod
modified theorem Prod.map_comp_map
modified theorem Prod.map_map
modified theorem Prod.mk.inj_left
modified theorem Prod.mk.inj_right
modified theorem MvQPF.Cofix.bisim'
modified def MvQPF.Const
modified def MvQPF.Fix
modified theorem Qpf.Cofix.bisim'
modified theorem Quot.eq
modified def Quot.factor
modified theorem Quot.factor_mk_eq
modified theorem Quotient.choice_eq
modified theorem Quotient.hrecOn'_mk''
modified theorem Quotient.hrecOn₂'_mk''
modified theorem Quotient.induction_on_pi
modified theorem Quotient.liftOn₂_mk
modified theorem Quotient.lift₂_mk
modified theorem Setoid.ext
modified theorem forall_quotient_iff
modified theorem surjective_quotient_mk
modified theorem RingHom.ext_rat
modified theorem Real.ciInf_const_zero
modified theorem Real.ciInf_empty
modified theorem Real.ciSup_const_zero
modified theorem Real.ciSup_empty
modified theorem Real.iInf_of_not_bddBelow
modified theorem Real.iSup_of_not_bddAbove
modified def CauSeq
modified def IsCauSeq
modified theorem rat_inv_continuous_lemma
modified theorem CauSeq.Completion.mk_smul
modified theorem ENNReal.coe_iInf
modified theorem ENNReal.coe_iSup
modified theorem ENNReal.iInf_ennreal
modified theorem ENNReal.iSup_coe_eq_top
modified theorem ENNReal.iSup_coe_lt_top
modified theorem ENNReal.iSup_ennreal
modified theorem ENNReal.iSup_eq_zero
modified theorem ENNReal.iSup_zero_eq_zero
modified def ENNReal.recTopCoe
modified theorem ENNReal.smul_def
modified theorem ENNReal.toNNReal_prod
modified theorem ENNReal.toReal_prod
modified theorem fibRec_charPoly_eq
modified theorem NNReal.coe_iInf
modified theorem NNReal.coe_iSup
modified theorem NNReal.iInf_const_zero
modified theorem NNReal.le_iInf_add_iInf
modified theorem NNReal.smul_def
modified def Rel
modified structure Semiquot
modified theorem Set.nontrivial_mono
modified theorem Set.subset_singleton_iff
modified theorem Set.subsingleton_isBot
modified theorem Set.subsingleton_isTop
modified theorem Subtype.mem
modified theorem Set.encard_mono
modified theorem Set.encard_univ
modified theorem Set.ncard_empty
modified theorem Set.ncard_univ
modified theorem Set.countable_isBot
modified theorem Set.countable_isTop
modified theorem Set.countable_pi
modified theorem Set.countable_univ_pi
modified theorem Finite.Set.finite_biUnion
modified theorem Set.Finite.iUnion
modified theorem Set.Finite.pi
modified theorem Set.Finite.sInter
modified theorem Set.finite_isBot
modified theorem Set.finite_isTop
modified def Set.fintypeBiUnion
modified theorem Set.iInf_iSup_of_antitone
modified theorem Set.iInf_iSup_of_monotone
modified theorem Set.iSup_iInf_of_antitone
modified theorem Set.iSup_iInf_of_monotone
modified theorem Set.iUnion_pi_of_monotone
modified theorem Set.apply_piecewise
modified theorem Set.apply_piecewise₂
modified theorem Set.eqOn_range
modified theorem Set.le_piecewise
modified theorem Set.pi_piecewise
modified theorem Set.piecewise_le
modified theorem Set.piecewise_le_piecewise
modified theorem Set.piecewise_mem_pi
modified theorem Set.piecewise_op
modified theorem Set.piecewise_op₂
modified theorem Set.piecewise_range_comp
modified theorem Set.univ_pi_piecewise
modified theorem Set.univ_pi_piecewise_univ
modified theorem Set.compl_range_some
modified theorem Set.insert_none_range_some
modified theorem Set.isCompl_range_some_none
modified theorem Set.range_eval
modified theorem Set.range_some_inter_none
modified theorem Set.range_some_union_none
modified theorem Set.subsingleton_of_image
modified theorem Set.subsingleton_range
modified theorem Set.subsingleton_Icc_iff
modified theorem iUnion_Ici_eq_Ici_iInf
modified theorem iUnion_Ici_eq_Ioi_iInf
modified theorem iUnion_Iic_eq_Iic_iSup
modified theorem iUnion_Iic_eq_Iio_iSup
modified theorem Set.mem_Icc_iff_abs_le
modified def orderIsoIooNegOneOne
modified theorem Set.ordConnected_biInter
modified theorem Set.ordConnected_iInter
modified theorem Set.ordConnected_image
modified theorem Set.ordConnected_of_Ioo
modified theorem Set.ordConnected_pi
modified theorem Set.ordConnected_preimage
modified theorem Set.ordConnected_range
modified theorem Set.ordConnected_singleton
modified theorem Set.Sigma.univ
modified theorem Set.biInter_inter
modified theorem Set.disjoint_iUnion_left
modified theorem Set.disjoint_iUnion_right
modified theorem Set.iInter_coe_set
modified theorem Set.iInter_subset_iInter₂
modified theorem Set.iUnion_coe_set
modified theorem Set.iUnion_of_singleton
modified theorem Set.iUnion_range_eq_sUnion
modified theorem Set.iUnion₂_subset_iUnion
modified theorem Set.image_projection_prod
modified theorem Set.inter_biInter
modified theorem Set.pairwiseDisjoint_pi
modified theorem Set.inv_range
modified theorem Set.nsmul_univ
modified theorem Set.finset_prod_singleton
modified theorem Set.list_prod_singleton
modified theorem Set.multiset_prod_singleton
modified theorem Set.range_smul_range
modified theorem Set.smul_set_range
modified def Set.diagonal
modified theorem Set.univ_pi_update
modified def SetSemiring
modified theorem Set.preimage_sigmaMap_sigma
modified structure IndexedPartition
modified theorem Setoid.card_classes_ker_le
modified theorem Setoid.finite_classes_ker
modified theorem Function.eq_of_sigmaMk_comp
modified theorem PSigma.subtype_ext
modified theorem PSigma.subtype_ext_iff
modified def Sigma.curry
modified theorem Sigma.curry_uncurry
modified theorem Sigma.subtype_ext
modified theorem Sigma.subtype_ext_iff
modified def Sigma.uncurry
modified theorem Sigma.uncurry_curry
modified theorem sign_sum
modified def Subtype.restrict
modified theorem Subtype.restrict_apply
modified theorem Subtype.surjective_restrict
modified def OrderIso.sumAssoc
modified def OrderIso.sumComm
modified theorem OrderIso.sumComm_symm
modified def OrderIso.sumLexAssoc
modified def Sym.Sym'
modified def Sym.cons'
modified theorem Sym.map_id'
modified theorem Sym.map_id
modified theorem Sym.map_map
modified def Sym.symEquivSym'
modified def Sym.toMultiset
modified def Sym
modified def Vector.Perm.isSetoid
modified theorem Sym.card_sym_eq_choose
modified theorem Sym.card_sym_eq_multichoose
modified def Sym2.equivMultiset
modified def Sym2.equivSym
modified def Tree.unitRecOn
modified structure TwoPointing
modified def TypeVec.Curry
modified def TypeVec.PredLast'
modified def TypeVec.PredLast
modified def TypeVec.RelLast'
modified def TypeVec.append1
modified def TypeVec.appendFun
modified theorem TypeVec.appendFun_aux
modified theorem TypeVec.appendFun_comp'
modified theorem TypeVec.appendFun_id_id
modified theorem TypeVec.appendFun_inj
modified theorem TypeVec.dropFun_appendFun
modified def TypeVec.dropRepeat
modified theorem TypeVec.drop_append1'
modified theorem TypeVec.drop_append1
modified theorem TypeVec.lastFun_appendFun
modified theorem TypeVec.last_append1
modified theorem ULift.ext_iff
modified structure UFNode
modified def Equiv.vectorEquivFin
modified def Vector.casesOn
modified def Vector.casesOn₂
modified def Vector.casesOn₃
modified theorem Vector.get_map
modified theorem Vector.head_map
modified def Vector.inductionOn
modified def Vector.inductionOn₂
modified def Vector.inductionOn₃
modified theorem Vector.tail_map
modified theorem Vector.toList_map
modified def Vector.revCasesOn
modified def Vector.revInductionOn
modified def WType.elim
modified theorem WType.elim_injective
modified inductive WType
modified theorem RingHom.ext_zmod
modified def ZMod.castHom
modified theorem ZMod.cast_neg_one
modified theorem ZMod.cast_sub_one
modified structure IsAddHom
modified structure IsMulHom
modified theorem MonoidHom.isGroupHom
modified theorem MulEquiv.isGroupHom
modified theorem Image.isSubfield
modified theorem IsSubfield.iInter
modified theorem Preimage.isSubfield
modified theorem Range.isSubfield
modified theorem Group.mem_closure_union_iff
modified def IsSubgroup.center
modified theorem IsSubgroup.iInter
modified def IsSubgroup.trivial
modified theorem IsSubmonoid.iInter
modified theorem IsSubmonoid.image
modified theorem IsSubmonoid.preimage
modified theorem Monoid.image_closure
modified theorem Range.isSubmonoid
modified theorem IsSubring.iInter
modified theorem Ring.image_closure
modified theorem birkhoffAverage_congr_ring'
modified theorem birkhoffAverage_congr_ring
modified theorem map_birkhoffAverage
modified theorem map_birkhoffSum
modified structure Flow
modified theorem mapsTo_omegaLimit'
modified theorem mapsTo_omegaLimit
modified theorem omegaLimit_image_eq
modified theorem omegaLimit_preimage_subset
modified theorem IntermediateField.coe_iInf
modified theorem CharP.sq_add_sq
modified theorem galois_poly_separable
modified theorem IntermediateField.aeval_coe
modified theorem IntermediateField.coe_prod
modified theorem IntermediateField.coe_sum
modified theorem IntermediateField.map_map
modified theorem IsAlgClosed.splits_codomain
modified theorem IsAlgClosed.splits_domain
modified theorem IntermediateField.map_id
modified theorem IntermediateField.map_mono
modified theorem finiteDimensional_sup
modified def finiteExts
modified def fixedByFinite
modified def galBasis
modified def galGroupBasis
modified theorem krullTopology_t2
modified theorem mem_galBasis_iff
modified theorem top_fixedByFinite
modified theorem minpoly.map_ne_one
modified theorem minpoly.add_algebraMap
modified theorem minpoly.eq_of_algebraMap_eq
modified theorem minpoly.sub_algebraMap
modified def PerfectClosure.liftOn
modified theorem AlgHom.card
modified theorem RatFunc.algebraMap_apply
modified theorem RatFunc.eval_algebraMap
modified theorem RatFunc.liftAlgHom_apply
modified theorem RatFunc.liftRingHom_apply
modified theorem RatFunc.map_apply
modified theorem RatFunc.map_apply_div
modified theorem RatFunc.map_denom_ne_zero
modified theorem IsSeparable.of_algHom
modified theorem Subfield.comap_iInf
modified theorem Subfield.map_iSup
modified theorem FiniteDimensional.left
modified theorem AffineIsometry.angle_map
modified theorem LinearIsometry.angle_map
modified theorem L_mul
modified theorem R_mul
modified theorem SmoothMap.coe_div
modified theorem SmoothMap.coe_inv
modified theorem SmoothMap.coe_mul
modified theorem SmoothMap.coe_one
modified theorem SmoothMap.coe_pow
modified theorem SmoothMap.coe_smul
modified def SmoothMap.evalRingHom
modified theorem SmoothMap.mul_comp
modified theorem SmoothMap.smul_comp'
modified theorem SmoothMap.smul_comp
modified def ChartedSpace.comp
modified structure ChartedSpaceCore
modified def ModelPi
modified def ModelProd
modified structure Pregroupoid
modified def Structomorph.refl
modified structure Structomorph
modified theorem chartAt_comp
modified theorem chartAt_self_eq
modified theorem chart_mem_atlas
modified theorem chartedSpaceSelf_atlas
modified def continuousGroupoid
modified def continuousPregroupoid
modified theorem mem_chart_source
modified theorem modelProd_range_prod_id
modified theorem piChartedSpace_chartAt
modified structure ModelWithCorners
modified def modelWithCornersSelf
modified theorem commProb_pi
modified theorem commProb_prod
modified theorem Con.coe_smul
modified theorem Con.hrec_on₂_coe
modified def Con.pi
modified theorem Con.quot_mk_eq_coe
modified theorem Con.smul
modified theorem RootableBy.surjective_pow
modified theorem Group.fg_of_surjective
modified theorem Monoid.fg_of_surjective
modified theorem Submonoid.FG.map
modified theorem Submonoid.FG.map_injective
modified theorem FreeGroup.ext_hom
modified theorem SMulCommClass.symm
modified theorem smul_eq_mul
modified def DomMulAct
modified theorem fixedPoints_subgroup_iSup
modified theorem fixedPoints_submonoid_iSup
modified theorem fixingSubgroup_iUnion
modified theorem fixingSubmonoid_iUnion
modified def AddAction.toPermHom
modified def arrowAction
modified theorem Function.extend_smul
modified theorem Function.update_smul
modified theorem Pi.faithfulSMul_at
modified theorem Pi.single_smul₀
modified theorem Pi.smul_apply'
modified theorem Set.piecewise_smul
modified theorem Prod.smul_mk_zero
modified theorem Prod.smul_zero_mk
modified theorem SetLike.forall_smul_mem_iff
modified theorem Subgroup.dvd_index_map
modified theorem Subgroup.index_comap
modified theorem Subgroup.index_iInf_le
modified theorem Subgroup.index_iInf_ne_zero
modified theorem Subgroup.index_map
modified theorem Subgroup.index_map_dvd
modified theorem Subgroup.index_map_eq
modified theorem Subgroup.relindex_comap
modified theorem Subgroup.relindex_iInf_le
modified theorem Localization.liftOn_zero
modified theorem Localization.liftOn₂_mk'
modified theorem Localization.liftOn₂_mk
modified theorem Group.IsNilpotent.nilpotent
modified theorem lowerCentralSeries.map
modified def lowerCentralSeries
modified theorem nilpotent_of_mulEquiv
modified theorem nilpotent_of_surjective
modified theorem upperCentralSeries.map
modified theorem IsOfFinOrder.apply
modified theorem Subgroup.pow_index_mem
modified theorem inf_eq_bot_of_coprime
modified theorem orderOf_dvd_nat_card
modified theorem orderOf_eq_orderOf_iff
modified theorem orderOf_injective
modified theorem orderOf_map_dvd
modified def powCardSubgroup
modified theorem powCoprime_inv
modified theorem powCoprime_one
modified theorem pow_card_eq_one'
modified theorem smul_eq_self_of_mem_zpowers
modified def subgroupOfIdempotent
modified def submonoidOfIdempotent
modified theorem IsPGroup.comap_of_injective
modified theorem IsPGroup.coprime_card_of_ne
modified theorem IsPGroup.map
modified theorem IsPGroup.of_equiv
modified theorem IsPGroup.of_injective
modified theorem IsPGroup.of_surjective
modified theorem Equiv.Perm.one_trans
modified theorem Equiv.Perm.sumCongr_inv
modified theorem Equiv.Perm.sumCongr_mul
modified theorem Equiv.Perm.sumCongr_one
modified theorem Equiv.Perm.trans_one
modified theorem Equiv.Perm.zpow_apply_comm
modified def MonoidHom.toHomPerm
modified theorem Equiv.Perm.IsCycle.swap_mul
modified theorem Equiv.optionCongr_one
modified theorem Equiv.optionCongr_sign
modified theorem Equiv.optionCongr_swap
modified theorem Finset.univ_perm_option
modified theorem map_equiv_removeNone
modified theorem QuotientGroup.map_comp_map
modified theorem QuotientGroup.map_map
modified theorem Equiv.Perm.not_solvable
modified theorem isSolvable_of_comm
modified theorem solvable_of_ker_le_range
modified theorem MonoidHom.map_cyclic
modified structure AddSubgroup
modified theorem CommGroup.center_eq_top
modified theorem MonoidHom.ker_prodMap
modified theorem Subgroup.closure_eq_bot_iff
modified theorem Subgroup.coe_iInf
modified def Subgroup.comap
modified theorem Subgroup.comap_iInf
modified theorem Subgroup.iSup_comap_le
modified theorem Subgroup.iSup_eq_closure
modified theorem Subgroup.map_iSup
modified theorem Subgroup.mem_iInf
modified theorem Subgroup.mem_iSup_of_mem
modified structure Subgroup
modified theorem Subgroup.noncommProd_mem
modified theorem Subgroup.Normal.conjAct
modified theorem Subgroup.iSup_induction'
modified theorem Subgroup.iSup_induction
modified theorem AddSubgroup.ker_saturated
modified theorem Int.range_castAddHom
modified structure AddSubmonoid
modified theorem IsUnit.mem_submonoid_iff
modified def IsUnit.submonoid
modified theorem Submonoid.coe_iInf
modified theorem Submonoid.iSup_eq_closure
modified theorem Submonoid.mem_iInf
modified theorem Submonoid.mem_iSup
modified structure Submonoid
modified theorem Submonoid.iSup_induction'
modified theorem Submonoid.iSup_induction
modified theorem Submonoid.map_powers
modified theorem Submonoid.mem_closure_pair
modified theorem Submonoid.mem_iSup_of_mem
modified theorem Submonoid.noncommProd_mem
modified theorem Submonoid.prod_mem
modified theorem prod_mem
modified theorem MonoidHom.mker_prod_map
modified def MonoidHom.restrict
modified theorem MonoidHom.restrict_apply
modified theorem Submonoid.comap_iInf
modified theorem Submonoid.map_iSup
modified theorem SubmonoidClass.coe_pow
modified theorem SubmonoidClass.mk_pow
modified theorem Submonoid.inv_iInf
modified theorem Submonoid.inv_iSup
modified theorem Submonoid.mem_closure_inv
modified structure AddSubsemigroup
modified theorem Subsemigroup.coe_iInf
modified theorem Subsemigroup.mem_iInf
modified theorem Subsemigroup.mem_iSup
modified structure Subsemigroup
modified theorem MulHom.prod_map_comap_prod'
modified def MulHom.restrict
modified theorem MulHom.restrict_apply
modified theorem Subsemigroup.comap_iInf
modified theorem Subsemigroup.map_iSup
modified theorem Sylow.pointwise_smul_def
modified theorem IsTorsionFree.prod
modified def Hamming
modified def ltByCases
modified structure AffineEquiv
modified theorem AffineMap.image_uIcc
modified structure AffineMap
modified theorem AffineMap.lineMap_mem
modified theorem AffineSubspace.comap_supr
modified theorem AffineSubspace.map_iSup
modified theorem AffineSubspace.span_iUnion
modified structure AffineSubspace
modified theorem affineIndependent_equiv
modified theorem AffineBasis.toMatrix_apply
modified theorem midpoint_unique
modified theorem homothety_invOf_two
modified theorem homothety_inv_two
modified theorem homothety_one_half
modified theorem lineMap_inv_two
modified theorem lineMap_one_half
modified theorem pi_midpoint_apply
modified theorem AffineMap.slope_comp
modified theorem LinearMap.slope_comp
modified theorem AlternatingMap.coe_pi
modified def AlternatingMap.pi
modified theorem LinearMap.smulRight_eq_comp
modified theorem Finsupp.smul_sum
modified theorem IsLinearMap.isLinearMap_sub
modified theorem LinearMap.coeFn_sum
modified theorem LinearMap.iInf_invariant
modified theorem LinearMap.map_sum
modified theorem LinearMap.range_neg
modified theorem Submodule.comap_iInf
modified theorem Submodule.map_iSup
modified def addMonoidHomLequivInt
modified def addMonoidHomLequivNat
modified theorem pi_eq_sum_univ
modified theorem Basis.basis_singleton_iff
modified theorem Basis.coe_finTwoProd_repr
modified theorem Basis.equiv_trans
modified theorem Basis.finTwoProd_one
modified theorem Basis.finTwoProd_zero
modified def Basis.groupSMul
modified theorem Basis.groupSMul_apply
modified theorem Basis.groupSMul_span_eq_top
modified theorem Basis.mem_span_repr_support
modified theorem Basis.singleton_apply
modified theorem Basis.singleton_repr
modified theorem BilinForm.comp_comp
modified structure BilinForm
modified theorem LinearMap.map_sum₂
modified theorem CliffordAlgebra.hom_ext
modified theorem toMatrix_dualTensorHom
modified theorem Submodule.dfinsupp_sum_mem
modified theorem Basis.det_reindex
modified theorem Basis.det_reindex_symm
modified theorem LinearEquiv.det_coe_symm
modified theorem LinearEquiv.isUnit_det'
modified theorem LinearMap.detAux_def''
modified theorem LinearMap.det_conj
modified theorem LinearMap.det_smul
modified theorem LinearMap.det_toMatrix'
modified theorem LinearMap.det_zero'
modified theorem LinearMap.det_zero
modified theorem LinearMap.isUnit_det
modified def equivOfPiLEquivPi
modified theorem Basis.le_span''
modified def Basis.ofRankEqZero
modified theorem Basis.ofRankEqZero_apply
modified theorem Ideal.rank_eq
modified theorem basis_le_span'
modified theorem linearIndependent_le_basis
modified theorem linearIndependent_le_span'
modified theorem linearIndependent_le_span
modified theorem Basis.eval_ker
modified theorem Basis.eval_range
modified theorem LinearEquiv.dualMap_trans
modified def FiniteDimensional
modified theorem finrank_eq_one_iff
modified theorem finrank_range_le_card
modified theorem finrank_span_eq_card
modified theorem Finsupp.domLCongr_apply
modified theorem Finsupp.domLCongr_single
modified theorem Finsupp.domLCongr_symm
modified theorem Finsupp.domLCongr_trans
modified theorem Finsupp.supported_iInter
modified theorem Finsupp.supported_iUnion
modified theorem Finsupp.total_total
modified theorem LinearMap.map_finsupp_total
modified theorem Finsupp.basis_repr
modified theorem Finsupp.coe_basis
modified theorem LinearMap.det_zero''
modified theorem Module.Finite.of_basis
modified structure Basis.SmithNormalForm
modified theorem Submodule.basisOfPid_bot
modified theorem Submodule.basis_of_pid_aux
modified theorem card_eq_of_linearEquiv
modified theorem card_le_of_injective'
modified theorem card_le_of_injective
modified theorem card_le_of_surjective'
modified theorem card_le_of_surjective
modified theorem linearIndependent_monoidHom
modified theorem Matrix.det_sum_le
modified theorem Matrix.det_sum_smul_le
modified theorem AlgHom.map_adjugate
modified theorem RingHom.map_adjugate
modified theorem Basis.toMatrix_map_vecMul
modified theorem Basis.toMatrix_mul_toMatrix
modified theorem matPolyEquiv_eq_x_pow_sub_c
modified theorem FiniteField.trace_pow_card
modified theorem Matrix.minpoly_dvd_charpoly
modified theorem charpoly_leftMulMatrix
modified theorem Matrix.det_blockDiagonal
modified theorem Matrix.det_unique
modified def MultilinearMap.pi
modified theorem MultilinearMap.sum_apply
modified theorem Basis.ext_multilinear
modified theorem Basis.ext_multilinear_fin
modified def LinearEquiv.funUnique
modified theorem LinearEquiv.funUnique_apply
modified theorem LinearMap.lsum_single
modified def LinearEquiv.prodComm
modified structure LinearMap.IsProj
modified theorem LinearMap.ofIsCompl_smul
modified theorem Projectivization.map_comp
modified theorem QuadraticForm.coeFn_sum
modified theorem QuadraticForm.polar_comp
modified theorem QuadraticForm.sum_apply
modified theorem Submodule.mapQ_comp
modified theorem RayVector.coe_neg
modified def RayVector
modified theorem SameRay.smul
modified theorem SModEq.eval
modified theorem LinearMap.ext_on_range
modified theorem Submodule.iSup_eq_span
modified theorem Submodule.iSup_induction'
modified theorem Submodule.iSup_induction
modified theorem Submodule.iSup_span
modified theorem Submodule.mem_iSup
modified theorem Submodule.span_iUnion₂
modified theorem Submodule.span_int_eq
modified theorem Submodule.sup_toAddSubgroup
modified theorem TensorAlgebra.hom_ext
modified def TensorAlgebra.lift
modified theorem TensorAlgebra.lift_comp_ι
modified theorem TensorAlgebra.lift_unique
modified theorem TensorAlgebra.lift_ι_apply
modified theorem TensorAlgebra.ι_comp_lift
modified def TensorPower
modified theorem TensorProduct.SMul.aux_of
modified theorem TensorProduct.sum_tmul
modified theorem TensorProduct.tmul_sum
modified theorem Classical.some_spec₂
modified theorem ExistsUnique.elim₂
modified theorem ExistsUnique.exists₂
modified theorem ExistsUnique.intro₂
modified theorem ExistsUnique.unique₂
modified def Function.swap₂
modified theorem PLift.down_inj
modified theorem PLift.down_injective
modified theorem congr_arg_heq
modified theorem exists₂_comm
modified theorem forall₂_swap
modified theorem forall₂_true_iff
modified theorem forall₃_true_iff
modified theorem heq_rec_iff_heq
modified def hidden
modified theorem imp_forall_iff
modified theorem ne_and_eq_iff_right
modified theorem ne_of_apply_ne
modified theorem rec_heq_iff_heq
modified theorem rec_heq_of_heq
modified theorem nonempty_denumerable
modified theorem nonempty_denumerable_iff
modified def Equiv.embeddingCongr
modified theorem Equiv.embeddingCongr_refl
modified theorem Equiv.embeddingCongr_symm
modified theorem Equiv.embeddingCongr_trans
modified theorem Equiv.refl_toEmbedding
modified theorem Equiv.trans_toEmbedding
modified theorem Function.Embedding.mk_coe
modified structure Function.Embedding
modified theorem Encodable.axiom_of_choice
modified theorem Encodable.skolem
modified def ULower
modified theorem nonempty_encodable
modified def Equiv.arrayEquivList
modified theorem Equiv.coe_sigmaUnique
modified def Equiv.funSplitAt
modified def Equiv.piComm
modified theorem Equiv.piComm_symm
modified def Equiv.piCongrLeft'
modified def Equiv.piCongrRight
modified def Equiv.piSplitAt
modified theorem Equiv.prodProdProdComm_symm
modified def Equiv.sigmaFiberEquiv
modified def Equiv.sigmaSumDistrib
modified def Equiv.sigmaUnique
modified theorem Equiv.sigmaUnique_apply
modified def Equiv.sumCompl
modified theorem Equiv.Perm.coe_subsingleton
modified def Equiv.Perm
modified def Equiv.arrowCongr'
modified theorem Equiv.arrowCongr'_refl
modified def Equiv.arrowCongr
modified theorem Equiv.arrowCongr_comp
modified theorem Equiv.arrowCongr_refl
modified def Equiv.equivOfIsEmpty
modified def Equiv.piSubsingleton
modified theorem Equiv.psigmaCongrRight_refl
modified theorem Equiv.psigmaCongrRight_symm
modified def Equiv.punitArrowEquiv
modified def Equiv.sigmaAssoc
modified def Equiv.sigmaCongrRight
modified theorem Equiv.sigmaCongrRight_refl
modified theorem Equiv.sigmaCongrRight_symm
modified theorem Equiv.sigmaCongrRight_trans
modified def Equiv.sigmaEquivProd
modified def Equiv.trueArrowEquiv
modified structure Equiv
modified def Equiv.codRestrict
modified theorem Fin.snoc_eq_cons_rotate
modified def finTwoArrowEquiv
modified def Encodable.fintypePi
modified theorem LocalEquiv.prod_trans
modified structure LocalEquiv
modified def Equiv.Set.rangeInl
modified def Equiv.Set.rangeInr
modified def Equiv.image
modified theorem Equiv.range_eq_univ
modified def Equiv.setCongr
modified theorem dite_comp_equiv_update
modified theorem Equiv.pow_def
modified theorem Equiv.smul_def
modified theorem Function.apply_update
modified theorem Function.apply_update₂
modified theorem Function.cantor_injective
modified theorem Function.comp_update
modified def Function.eval
modified theorem Function.eval_apply
modified theorem Function.funext_iff
modified theorem Function.ne_iff
modified theorem Function.update_apply
modified theorem Function.update_comm
modified theorem Function.update_idem
modified def Set.SeparatesPoints
modified theorem eq_rec_inj
modified theorem eq_rec_on_bijective
modified def Function.Iterate.rec
modified theorem Function.Iterate.rec_zero
modified def isEmptyElim
modified theorem isEmpty_pi
modified theorem isEmpty_prod
modified theorem isEmpty_psigma
modified theorem isEmpty_sigma
modified theorem Classical.nonempty_pi
modified theorem Nonempty.elim_to_inhabited
modified theorem exists_true_iff_nonempty
modified theorem nonempty_psigma
modified theorem not_nonempty_iff_imp_false
modified theorem exists_pair_lt
modified theorem exists_pair_ne
modified theorem subsingleton_or_nontrivial
modified theorem small_congr
modified theorem small_map
modified def uniqueOfSubsingleton
modified theorem AEMeasurable.nnreal_tsum
modified theorem borel_eq_generateFrom_Ico
modified theorem borel_eq_generateFrom_Ioc
modified theorem measurable_ciInf
modified theorem measurable_ciSup
modified theorem pi_le_borel_pi
modified theorem Continuous.map_borel_eq
modified theorem Continuous.map_eq_borel
modified theorem IsOpen.analyticSet_image
modified theorem MeasurableSet.analyticSet
modified theorem MeasurableEmbedding.prod_mk
modified structure Besicovitch.BallPackage
modified structure Besicovitch.SatelliteConfig
modified structure Besicovitch.TauPackage
modified theorem essSup_mono_measure'
modified def MeasureTheory.Lp
modified theorem MeasureTheory.snorm_aeeqFun
modified theorem aestronglyMeasurable_id
modified theorem aemeasurable_inv_iff
modified theorem aemeasurable_inv_iff₀
modified theorem measurable_div_const'
modified theorem measurable_inv_iff
modified theorem measurable_inv_iff₀
modified theorem measurable_mul_op
modified theorem measurable_mul_unop
modified theorem MeasurableSet.const_smul
modified theorem MeasurableSet.const_smul₀
modified theorem MeasureTheory.integral_div
modified theorem Set.disjoint_sdiff_inter
modified theorem integral_smul_const
modified theorem torusIntegral_smul
modified theorem Finset.measurable_sup'
modified structure MeasurableEmbedding
modified def MeasurableEquiv.refl
modified theorem MeasurableEquiv.symm_refl
modified structure MeasurableEquiv
modified structure MeasurableSpace
modified theorem Filter.Tendsto.mass
modified theorem integral_comp_neg_Iic
modified theorem integral_comp_neg_Ioi
modified theorem Finset.measure_zero
modified theorem Set.Countable.ae_not_mem
modified theorem Set.Countable.measure_zero
modified theorem Set.Finite.measure_zero
modified structure MeasureTheory.Measure
modified theorem MeasureTheory.ae_all_iff
modified theorem Set.mulIndicator_ae_eq_one
modified structure MeasureTheory.OuterMeasure
modified theorem MeasureTheory.extend_congr
modified theorem MeasureTheory.extend_top
modified theorem rightLim_eq_of_tendsto
modified theorem rightLim_eq_sInf
modified structure MeasureTheory.VectorMeasure
modified structure MeasurableSpace.DynkinSystem
modified theorem Set.definable_finset_inf
modified theorem Set.definable_finset_sup
modified theorem dvd_sub_pow_of_dvd_sub
modified theorem ClassGroup.norm_lt
modified theorem IsCyclotomicExtension.equiv
modified theorem Nat.Prime.prod_divisors
modified theorem Nat.prod_div_divisors
modified theorem Nat.prod_divisors_prime_pow
modified theorem functionField_iff
modified theorem Char.card_pow_card
modified theorem FiniteField.two_pow_card
modified theorem jacobiSym.value_at
modified def quadraticCharFun
modified theorem quadraticChar_card_card
modified theorem SlashAction.neg_slash
modified def monoidHomSlashAction
modified theorem padicNorm.sum_le'
modified theorem padicNorm.sum_le
modified theorem padicNorm.sum_lt'
modified theorem padicNorm.sum_lt
modified theorem euler_four_squares
modified def approxOrderOf
modified theorem mem_approxOrderOf_iff
modified theorem mem_wellApproximable_iff
modified def wellApproximable
modified def OrderDual
modified theorem Preorder.toLE_injective
modified theorem not_bddAbove_iff
modified theorem not_bddBelow_iff
modified theorem BddDistLatCat.coe_of
modified def BddDistLatCat.of
modified theorem BddLatCat.coe_of
modified def BddLatCat.of
modified theorem BddOrdCat.coe_of
modified def BddOrdCat.of
modified theorem BoolAlgCat.coe_of
modified def BoolAlgCat.of
modified theorem CompleteLatCat.coe_of
modified def CompleteLatCat.of
modified theorem DistLatCat.coe_of
modified def DistLatCat.of
modified def FinBddDistLatCat.of'
modified def FinBddDistLatCat.of
modified theorem FinBoolAlgCat.coe_of
modified def FinBoolAlgCat.of
modified theorem FinPartOrd.coe_of
modified def FinPartOrd.of
modified theorem FrmCat.coe_of
modified def FrmCat.of
modified theorem HeytAlgCat.coe_of
modified def HeytAlgCat.of
modified theorem LatCat.coe_of
modified def LatCat.of
modified theorem LinOrdCat.coe_of
modified def LinOrdCat.of
modified theorem NonemptyFinLinOrdCat.coe_of
modified theorem ωCPO.coe_of
modified def ωCPO.of
modified theorem PartOrdCat.coe_of
modified def PartOrdCat.of
modified theorem PreordCat.coe_of
modified def PreordCat.of
modified theorem SemilatInfCat.coe_of
modified def SemilatInfCat.of
modified theorem SemilatSupCat.coe_of
modified def SemilatSupCat.of
modified structure Flag
modified def LE.toBtw
modified def LT.toSBtw
modified theorem biInf_sup_biInf
modified theorem biSup_inf_biSup
modified theorem iInf_sup_iInf
modified theorem iInf_sup_of_antitone
modified theorem iInf_sup_of_monotone
modified theorem iSup_inf_iSup
modified theorem iSup_inf_of_antitone
modified theorem iSup_inf_of_monotone
modified theorem binary_relation_sInf_iff
modified theorem binary_relation_sSup_iff
modified def completeLatticeOfInf
modified def completeLatticeOfSup
modified theorem iInf_apply
modified theorem iInf_le_iInf₂
modified theorem iInf_sigma
modified theorem iInf₂_comm
modified theorem iSup_apply
modified theorem iSup_comp_le
modified theorem iSup_sigma
modified theorem iSup₂_comm
modified theorem iSup₂_le_iSup
modified theorem le_iInf_comp
modified theorem sInf_apply
modified theorem sSup_apply
modified theorem unary_relation_sInf_iff
modified theorem unary_relation_sSup_iff
modified theorem Monotone.map_csInf
modified theorem MonotoneOn.map_csInf
modified theorem WithBot.ciSup_empty
modified theorem WithBot.csSup_empty
modified theorem WithTop.iInf_empty
modified theorem WithTop.iSup_coe_eq_top
modified theorem WithTop.iSup_coe_lt_top
modified theorem WithTop.isGLB_sInf'
modified theorem WithTop.isLUB_sSup'
modified theorem WithTop.sInf_empty
modified theorem ciSup_set_le_iff
modified theorem le_ciInf_set_iff
modified theorem apply_covby_apply_iff
modified theorem apply_wcovby_apply_iff
modified def Complementeds
modified def disjointedRec
modified theorem disjointedRec_zero
modified def WellOrderExtension
modified theorem Filter.prod_map_atBot_eq
modified theorem Filter.prod_map_atTop_eq
modified structure Filter.CountableFilterBasis
modified theorem Filter.HasBasis.coprod
modified theorem Filter.HasBasis.inf
modified theorem Filter.HasBasis.prod
modified theorem Filter.HasBasis.sup
modified theorem Filter.hasBasis_iInf'
modified theorem Filter.hasBasis_iInf
modified theorem Filter.hasBasis_iSup
modified theorem Filter.map_sigma_mk_comap
modified structure FilterBasis
modified theorem Filter.comap_eval_neBot
modified theorem Filter.comap_eval_neBot_iff
modified theorem Filter.eventually_all
modified theorem Filter.forall_in_swap
modified def Filter.giGenerate
modified theorem Filter.iInf_sets_eq_finite
modified theorem Filter.mem_iInf_finite
modified theorem Filter.mem_iInf_of_finite
modified structure Filter
modified theorem Filter.coprodᵢ_cofinite
modified theorem countable_bInter_mem
modified theorem eventually_countable_ball
modified theorem exists_countable_separating
modified theorem exists_seq_separating
modified theorem IsExtrFilter.congr
modified theorem IsMaxFilter.congr
modified theorem IsMinFilter.congr
modified def Filter.Germ.liftOn
modified def Filter.Germ
modified def Filter.Product
modified def Filter.germSetoid
modified def Filter.productSetoid
modified theorem Filter.tendsto_pi
modified theorem Filter.Tendsto.prod_map
modified theorem Filter.prod_map_map_eq'
modified theorem Filter.tendsto_prod_swap
modified structure Ultrafilter
modified theorem Filter.BoundedAtFilter.smul
modified theorem Filter.ZeroAtFilter.smul
modified structure GaloisInsertion
modified def Prod.GameAdd.fix
modified theorem Prod.GameAdd.fix_eq
modified def Sym2.GameAdd.fix
modified theorem Sym2.GameAdd.fix_eq
modified structure BiheytingHom
modified structure CoheytingHom
modified structure HeytingHom
modified theorem OrderHom.comp_const
modified def OrderHom.const
modified def OrderHom.dualIso
modified structure OrderHom
modified def OrderIso.funUnique
modified def OrderIso.ofHomInv
modified def OrderIso.refl
modified theorem OrderIso.symm_refl
modified structure BotHom
modified structure BoundedOrderHom
modified structure TopHom
modified structure CompleteLatticeHom
modified structure FrameHom
modified structure sInfHom
modified structure sSupHom
modified structure BoundedLatticeHom
modified structure InfHom
modified structure InfTopHom
modified structure LatticeHom
modified structure SupBotHom
modified structure SupHom
modified theorem OrderHom.coe_iInf
modified theorem OrderHom.coe_iSup
modified theorem OrderHom.iInf_apply
modified theorem OrderHom.iSup_apply
modified structure InitialSeg
modified theorem PrincipalSeg.ofElement_top
modified structure PrincipalSeg
modified def Interval
modified structure NonemptyInterval
modified def Lattice.mk'
modified theorem SemilatticeInf.dual_dual
modified def SemilatticeInf.mk'
modified theorem SemilatticeSup.dual_dual
modified def SemilatticeSup.mk'
modified theorem Filter.liminf_congr
modified theorem Filter.liminf_const
modified theorem Filter.liminf_eq_sSup_sInf
modified theorem Filter.liminf_le_liminf
modified theorem Filter.limsup_congr
modified theorem Filter.limsup_const
modified theorem Filter.limsup_eq_sInf_sSup
modified theorem Filter.limsup_le_limsup
modified theorem NoBotOrder.to_noMinOrder
modified theorem NoTopOrder.to_noMaxOrder
modified theorem noBotOrder_iff_noMinOrder
modified theorem noTopOrder_iff_noMaxOrder
modified structure Order.Ideal.PrimePair
modified def IsWellFounded.fix
modified theorem IsWellFounded.fix_eq
modified theorem WellFounded.asymmetric
modified def WellFoundedGT.fix
modified theorem WellFoundedGT.fix_eq
modified def WellFoundedGT
modified def WellFoundedLT.fix
modified theorem WellFoundedLT.fix_eq
modified def WellFoundedLT
modified theorem wellFoundedGT_dual_iff
modified theorem wellFoundedLT_dual_iff
modified structure RelEmbedding
modified structure RelHom
modified structure RelIso
modified def Subtype.relEmbedding
modified theorem Finset.SupIndep.sigma
modified def Lex
modified structure LowerSet
modified structure UpperSet
modified theorem WellFounded.onFun
modified theorem Pi.isPwo
modified def WithBot.recBotCoe
modified theorem WithBot.recBotCoe_bot
modified theorem WithBot.recBotCoe_coe
modified def WithBot
modified def WithTop.recTopCoe
modified theorem WithTop.recTopCoe_coe
modified theorem WithTop.recTopCoe_top
modified def WithTop
modified theorem IsAtomic.of_isChain_bounded
modified theorem atBot_le_nhds_bot
modified theorem atTop_le_nhds_top
modified theorem tendsto_of_antitone
modified def Pmf.uniformOfFintype
modified structure MeasureTheory.Filtration
modified theorem Action.sum_hom
modified theorem Algebra.adjoin_iUnion
modified theorem lift_of_splits
modified theorem Algebra.fg_trans'
modified theorem Basis.algebraMap_injective
modified theorem ClassGroup.equiv_mk
modified structure RingCon
modified theorem IsCoprime.sq_add_sq_ne_zero
modified theorem Ideal.IsPrime.isMaximal
modified theorem isDedekindDomain_iff
modified theorem Ideal.prod_le_prime
modified theorem Derivation.leibniz_inv
modified theorem Derivation.map_sum
modified structure Derivation
modified theorem Ideal.Filtration.iInf_N
modified theorem Ideal.Filtration.iSup_N
modified theorem Ideal.FG.map
modified theorem Ideal.fg_ker_comp
modified theorem Module.Finite.trans
modified theorem Submodule.fg_biSup
modified theorem Submodule.fg_finset_sup
modified theorem Submodule.fg_iSup
modified theorem Submodule.fg_induction
modified theorem Submodule.fg_ker_comp
modified theorem Submodule.fg_of_fg_map
modified theorem Submodule.fg_of_isUnit
modified theorem Submodule.fg_pi
modified theorem Submodule.fg_unit
modified theorem card_units_lt
modified theorem Ideal.IsHomogeneous.iInf₂
modified theorem Ideal.IsHomogeneous.iSup₂
modified structure HahnSeries.SummableFamily
modified structure HahnSeries
modified theorem Ideal.bot_prime
modified theorem Ideal.mem_iInf
modified theorem Ideal.mem_iSup_of_mem
modified theorem Ideal.mul_sub_mul_mem
modified theorem Ideal.span_singleton_ne_top
modified theorem Ideal.sum_mem
modified theorem RingHom.domain_localRing
modified def minimalPrimes
modified theorem Ideal.map_relNorm
modified theorem Ideal.map_spanNorm
modified theorem Ideal.natAbs_det_equiv
modified theorem Ideal.spanNorm_mul_of_field
modified theorem Associates.mk_ne_zero'
modified theorem Basis.mem_ideal_iff'
modified theorem Basis.mem_ideal_iff
modified theorem Ideal.coe_restrictScalars
modified theorem Ideal.comap_comap
modified theorem Ideal.iInf_span_singleton
modified theorem Ideal.map_isPrime_of_equiv
modified theorem Ideal.map_map
modified theorem Ideal.mul_eq_bot
modified theorem Ideal.prod_eq_bot
modified theorem Ideal.prod_mem_prod
modified theorem Ideal.prod_span
modified theorem Ideal.prod_span_singleton
modified theorem Ideal.restrictScalars_mul
modified theorem Ideal.smul_top_eq_map
modified theorem Ideal.sum_eq_sup
modified theorem RingHom.ker_equiv
modified theorem RingHom.ker_isPrime
modified theorem Submodule.smul_iInf_le
modified theorem Submodule.smul_iSup
modified theorem Ideal.map_pi
modified def Ideal.quotEquivOfEq
modified theorem Ideal.quotEquivOfEq_mk
modified theorem Ideal.quotEquivOfEq_symm
modified theorem IsIntegral.det
modified theorem IsIntegral.prod
modified theorem IsIntegral.sum
modified theorem Module.End.isIntegral
modified theorem integralClosure_idem
modified theorem isIntegral_algEquiv
modified theorem isIntegral_algHom_iff
modified theorem isIntegral_of_mem_closure''
modified theorem map_isIntegral
modified theorem map_isIntegral_int
modified theorem card_fiber_eq_of_mem_range
modified theorem IsAdjoinRoot.aequiv_aequiv
modified theorem IsAdjoinRoot.aequiv_ofEquiv
modified theorem IsAdjoinRoot.aequiv_trans
modified theorem IsAdjoinRoot.liftHom_aequiv
modified theorem IsAdjoinRoot.lift_aequiv
modified theorem IsAdjoinRoot.ofEquiv_aequiv
modified theorem Algebra.pushoutDesc_apply
modified theorem Algebra.pushoutDesc_left
modified theorem Algebra.pushoutDesc_right
modified theorem PowerSeries.coe_smul
modified theorem IsLocalization.map_comp_map
modified theorem IsLocalization.map_id_mk'
modified theorem IsLocalization.map_map
modified theorem Localization.mk_algebraMap
modified theorem Localization.mk_sum
modified theorem isIntegral_localization'
modified theorem IsLocalization.mem_span_iff
modified theorem multiplicity.Finset.prod
modified theorem IsNilpotent.map
modified theorem isReduced_of_injective
modified def nilradical
modified theorem nilradical_eq_sInf
modified theorem nilradical_eq_zero
modified theorem NonUnitalSubring.coe_iInf
modified theorem NonUnitalSubring.comap_iInf
modified theorem NonUnitalSubring.map_iSup
modified theorem NonUnitalSubring.mem_iInf
modified def nonZeroDivisors
modified def OreLocalization
modified theorem Polynomial.cyclotomic'_one
modified theorem Polynomial.cyclotomic'_two
modified theorem Polynomial.cyclotomic'_zero
modified theorem Polynomial.cyclotomic.monic
modified def Polynomial.cyclotomic
modified theorem Polynomial.cyclotomic_one
modified theorem Polynomial.cyclotomic_prime
modified theorem Polynomial.cyclotomic_three
modified theorem Polynomial.cyclotomic_two
modified theorem Polynomial.cyclotomic_zero
modified theorem Polynomial.map_cyclotomic
modified theorem isRoot_of_unity_iff
modified theorem factorial_mul_pochhammer
modified theorem pochhammer_eval_one
modified theorem pochhammer_succ_eval
modified theorem PowerBasis.algHom_ext
modified structure PowerBasis
modified def MvPowerSeries
modified theorem PowerSeries.coeff_smul
modified def PowerSeries
modified theorem mul_eq_mul_prime_prod
modified def primitiveRoots
modified def rootsOfUnity
modified theorem Subring.coe_iInf
modified theorem Subring.comap_iInf
modified theorem Subring.map_iSup
modified theorem Subring.mem_iInf
modified theorem Units.mem_posSubgroup
modified def Units.posSubgroup
modified theorem Subsemiring.comap_iInf
modified theorem Subsemiring.map_iSup
modified theorem mem_posSubmonoid
modified def posSubmonoid
modified theorem Algebra.traceMatrix_reindex
modified theorem Associates.quot_out
modified theorem AddValuation.IsEquiv.comap
modified def AddValuation.comap
modified theorem AddValuation.comap_comp
modified theorem AddValuation.map_le_sum
modified theorem AddValuation.map_lt_sum'
modified theorem AddValuation.map_lt_sum
modified theorem Valuation.IsEquiv.comap
modified def Valuation.comap
modified theorem Valuation.comap_apply
modified theorem Valuation.comap_comp
modified theorem Valuation.comap_supp
modified theorem Valuation.map_sum_le
modified theorem Valuation.map_sum_lt'
modified theorem Valuation.map_sum_lt
modified theorem AddValuation.comap_supp
modified def WittVector.mk
modified structure WittVector
modified theorem wittStructureInt_rename
modified theorem TruncatedWittVector.card
modified def TruncatedWittVector
modified theorem aeval_wittPolynomial
modified theorem Cardinal.eq_one_iff_unique
modified theorem Cardinal.mk_eq_aleph0
modified theorem Cardinal.mk_sigma
modified theorem Cardinal.three_le
modified theorem Cardinal.mk_bounded_subset
modified theorem Nat.card_eq_of_equiv_fin
modified theorem Nat.card_pi
modified theorem Nat.card_plift
modified theorem Nat.card_prod
modified theorem Nat.card_ulift
modified def Nat.equivFinOfCardPos
modified def PartENat.card
modified theorem PartENat.card_congr
modified theorem PartENat.card_pLift
modified theorem PartENat.card_sum
modified theorem PartENat.card_uLift
modified theorem Cardinal.aleph0_mul_mk_eq
modified theorem Cardinal.extend_function
modified theorem Cardinal.mk_add_one_eq
modified theorem Cardinal.mk_mul_aleph0_eq
modified def PGame.moveRecOn
modified def Finsets
modified def Lists.inductionMut
modified def Lists
modified def Ordinal.limitRecOn
modified theorem Ordinal.CNFRec_pos
modified theorem Ordinal.CNFRec_zero
modified def NONote.recOn
modified theorem Subtype.exists_pi_extension
modified theorem HasCompactSupport.comp_smul
modified theorem IsClosed.smul₀
modified theorem isClosedMap_smul₀
modified theorem Units.embedding_val_mk'
modified theorem Units.embedding_val_mk
modified structure ContinuousAffineMap
modified structure ContinuousAddMonoidHom
modified structure ModuleFilterBasis
modified theorem ContinuousInv.of_nhds_one
modified theorem Filter.HasBasis.nhds_of_one
modified theorem Inducing.continuousInv
modified theorem TopologicalGroup.ext
modified theorem TopologicalGroup.ext_iff
modified theorem tendsto_div_nhds_one_iff
modified theorem topologicalGroup_induced
modified theorem AddMonoidHom.completion_add
modified theorem HasSum.sigma
modified theorem HasSum.sigma_of_hasSum
modified theorem HasSum.sum_nat_of_sum_int
modified theorem HasSum.update'
modified theorem Summable.sigma'
modified theorem Summable.sigma
modified theorem Summable.sigma_factor
modified theorem eq_add_of_hasSum_ite
modified theorem tsum_sigma'
modified theorem tsum_sigma
modified structure ContinuousAlternatingMap
modified structure ContinuousLinearEquiv
modified theorem ContinuousLinearMap.coe_sum
modified structure ContinuousLinearMap
modified theorem LinearMap.continuous_on_pi
modified theorem continuous_equivFun_basis
modified theorem LocallyConvexSpace.ofBases
modified def starL'
modified def starL
modified def WeakDual
modified theorem Inducing.continuousMul
modified theorem continuousMul_induced
modified theorem eventuallyEq_prod
modified theorem finprod_eventually_eq_prod
modified theorem is_bot_adic_iff
modified theorem RingSubgroupsBasis.of_comm
modified structure RingSubgroupsBasis
modified structure OpenAddSubgroup
modified theorem OpenSubgroup.comap_comap
modified structure OpenSubgroup
modified theorem isCompact_uIcc
modified theorem TopologicalRing.of_norm
modified theorem isBounded_ge_atTop
modified theorem isBounded_le_atBot
modified theorem tendsto_of_monotone
modified def AbsoluteValue.comp
modified theorem CauchySeq.const_mul
modified theorem CauchySeq.inv
modified theorem CauchySeq.mul
modified theorem CauchySeq.mul_const
modified theorem UniformGroup.ext
modified theorem UniformGroup.ext_iff
modified theorem uniformGroup_comap
modified theorem uniformGroup_iInf
modified theorem isTopologicalBasis_iInf
modified theorem isTopologicalBasis_pi
modified theorem Finset.closure_biUnion
modified theorem Finset.interior_iInter
modified def MapClusterPt
modified theorem OrderTop.tendsto_atTop_nhds
modified theorem closure_iUnion
modified theorem interior_Inter₂_subset
modified theorem interior_iInter
modified theorem mapClusterPt_iff
modified theorem mapClusterPt_of_comp
modified theorem monotone_closure
modified theorem tendsto_pure_nhds
modified def Bornology.cobounded
modified theorem Bornology.le_cofinite
modified def Bornology.ofBounded'
modified def Bornology.ofBounded
modified def Bornology.induced
modified theorem Bornology.isBounded_induced
modified theorem boundedSpace_induced_iff
modified structure LocallyBoundedMap
modified def Born.of
modified def Compactum.forget
modified def Compactum.free
modified theorem Locale.coe_of
modified def Locale.of
modified def Profinite.of
modified def Stonean.of
modified theorem OnePoint.continuousAt_coe
modified theorem OnePoint.continuousAt_infty
modified theorem OnePoint.tendsto_nhds_infty
modified def OnePoint
modified theorem IsPreconnected.constant
modified theorem PreconnectedSpace.constant
modified theorem isPreconnected_iUnion
modified def CofiniteTopology
modified theorem Continuous.fin_insertNth
modified theorem ContinuousAt.fin_insertNth
modified theorem DenseRange.prod_map
modified theorem DiscreteTopology.of_subset
modified theorem Filter.HasBasis.prod_nhds'
modified theorem Filter.HasBasis.prod_nhds
modified theorem continuous_apply_apply
modified theorem induced_to_pi
modified theorem inducing_iInf_to_pi
modified theorem pi_generateFrom_eq
modified theorem pi_generateFrom_eq_finite
modified theorem tendsto_subtype_rng
modified theorem ContinuousMap.coe_prod
modified theorem ContinuousMap.hasSum_apply
modified theorem ContinuousMap.prod_apply
modified theorem ContinuousMap.tsum_apply
modified def continuousSubgroup
modified def continuousSubmonoid
modified def continuousSubring
modified def continuousSubsemiring
modified def ContinuousMap.sigmaMk
modified structure ContinuousMap
modified theorem ContinuousMap.inf'_apply
modified theorem ContinuousMap.inf'_coe
modified theorem ContinuousMap.sup'_apply
modified theorem ContinuousMap.sup'_coe
modified theorem ContinuousOn.if
modified theorem ContinuousOn.mono_dom
modified theorem ContinuousOn.mono_rng
modified theorem DenseRange.nhdsWithin_neBot
modified theorem closure_pi_set
modified theorem continuousOn_pi
modified theorem continuousWithinAt_pi
modified theorem continuous_of_cover_nhds
modified theorem dense_pi
modified theorem mem_closure_pi
modified theorem nhdsWithin_pi_eq'
modified theorem nhdsWithin_pi_eq
modified theorem nhdsWithin_pi_eq_bot
modified theorem nhdsWithin_pi_neBot
modified theorem nhdsWithin_pi_univ_eq
modified theorem nhdsWithin_prod
modified theorem principal_subtype
modified theorem IsCoveringMap.mk
modified theorem IsCoveringMapOn.mk
modified def IsEvenlyCovered
modified theorem denseEmbedding_id
modified structure DiscreteQuotient
modified structure FiberBundleCore
modified def residual
modified structure ContinuousOpenMap
modified def Homeomorph.Set.univ
modified def Homeomorph.funUnique
modified def Homeomorph.piSplitAt
modified structure Homeomorph
modified theorem id_nullhomotopic
modified def Cube.boundary
modified def HomotopyGroup.Pi
modified def HomotopyGroup
modified theorem ENNReal.add_biSup'
modified theorem ENNReal.add_iSup
modified theorem ENNReal.biSup_add'
modified theorem ENNReal.iSup_add
modified theorem ENNReal.iSup_add_iSup
modified theorem ENNReal.iSup_add_iSup_le
modified theorem ENNReal.iSup_div
modified theorem ENNReal.iSup_mul
modified theorem ENNReal.inv_map_iInf
modified theorem ENNReal.inv_map_iSup
modified theorem ENNReal.mul_iSup
modified theorem ENNReal.smul_iSup
modified theorem ENNReal.sub_iSup
modified theorem ENNReal.tsum_biUnion_le
modified theorem ENNReal.tsum_iSup_eq
modified theorem ENNReal.tsum_iUnion_le
modified theorem ENNReal.tsum_iUnion_le_tsum
modified theorem Metric.diam_closure
modified theorem NNReal.summable_sigma
modified theorem summable_of_sum_le
modified theorem summable_sigma_of_nonneg
modified theorem tsum_comp_le_tsum_of_inj
modified theorem EReal.tendsto_coe
modified theorem EReal.tendsto_coe_ennreal
modified theorem Filter.Tendsto.cons
modified theorem List.tendsto_cons_iff
modified theorem List.tendsto_nhds
modified theorem LocalHomeomorph.prod_trans
modified structure LocalHomeomorph
modified theorem IsLocallyConstant.comp₂
modified theorem IsLocallyConstant.desc
modified theorem LocallyConstant.coe_desc
modified def LocallyConstant.const
modified def LocallyConstant.desc
modified def LocallyConstant.flip
modified theorem LocallyConstant.flip_unflip
modified theorem LocallyConstant.map_comp
modified theorem LocallyConstant.unflip_flip
modified structure LocallyConstant
modified theorem Embedding.discreteTopology
modified theorem Embedding.tendsto_nhds_iff
modified theorem Inducing.tendsto_nhds_iff
modified def QuotientMap
modified def Bornology.ofDist
modified theorem Filter.Tendsto.congr_dist
modified theorem Metric.isOpen_singleton_iff
modified theorem Metric.tendstoUniformly_iff
modified theorem MetricSpace.ext
modified theorem PseudoMetricSpace.ext
modified theorem edist_lt_top
modified theorem isCompact_sphere
modified theorem tendsto_iff_of_dist
modified theorem Dilation.comp_assoc
modified theorem Dilation.dist_eq
modified theorem Dilation.nndist_eq
modified theorem Dilation.tendsto_nhds_iff
modified def DilationEquiv.refl
modified structure DilationEquiv
modified theorem EMetric.diam_pi_le_of_le
modified theorem Metric.equicontinuousAt_iff
modified theorem Real.dimH_univ_pi
modified theorem Metric.Bounded.cthickening
modified theorem Metric.diam_cthickening_le
modified theorem Metric.diam_thickening_le
modified theorem Set.le_einfsep_pi_of_le
modified theorem Isometry.tendsto_nhds_iff
modified theorem isometry_dcomp
modified def IsMetricSeparated
modified def PiNat.longestPrefix
modified theorem IsClosed.polishSpace
modified theorem IsOpen.polishSpace
modified def PolishSpace.AuxCopy
modified theorem complete_polishSpaceMetric
modified def polishSpaceMetric
modified def upgradePolishSpace
modified theorem Equiv.coinduced_symm
modified theorem Equiv.induced_symm
modified theorem discreteTopology_bot
modified theorem forall_open_iff_discrete
modified theorem le_iff_nhds
modified theorem le_nhdsAdjoint_iff'
modified theorem le_nhdsAdjoint_iff
modified theorem nhdsAdjoint_nhds
modified theorem nhdsAdjoint_nhds_of_ne
modified theorem nhds_discrete
modified theorem nhds_iInf
modified def Preorder.topology
modified theorem exists_seq_tendsto_sInf
modified theorem exists_seq_tendsto_sSup
modified theorem orderTopology_of_nhds_abs
modified structure ContinuousOrderHom
modified structure EsakiaHom
modified structure PseudoEpimorphism
modified structure BumpCovering
modified structure PartitionOfUnity
modified theorem Filter.Tendsto.path_extend
modified theorem IsPathConnected.image'
modified theorem IsPathConnected.image
modified theorem Path.extend_extends'
modified theorem Path.extend_extends
modified theorem Path.extend_of_le_zero
modified theorem Path.extend_of_one_le
modified theorem Path.extend_range
modified def Path.map'
modified def Path.map
modified theorem Path.map_coe
modified theorem Path.map_map
modified theorem Path.map_symm
modified theorem Path.map_trans
modified theorem Path.refl_extend
modified theorem Path.refl_trans_refl
modified theorem Path.symm_cast
modified theorem Path.symm_continuous_family
modified theorem Path.trans_cast
modified theorem Path.trans_range
modified def Path.truncate
modified def Path.truncateOfLE
modified theorem Path.truncate_one_one
modified theorem Path.truncate_range
modified theorem Path.truncate_self
modified theorem Path.truncate_zero_one
modified theorem Path.truncate_zero_zero
modified theorem IsProperMap.pi_map
modified theorem isQuasiSeparated_univ
modified theorem isQuasiSeparated_univ_iff
modified theorem RegularSpace.ofBasis
modified theorem biInter_basis_nhds
modified theorem discrete_of_t1_of_finite
modified theorem separated_by_continuous
modified theorem separated_by_openEmbedding
modified def specializationOrder
modified theorem t1Space_antitone
modified structure TopologicalSpace.Clopens
modified structure TopologicalSpace.Closeds
modified structure TopologicalSpace.CompactOpens
modified structure TopologicalSpace.Compacts
modified structure ClopenUpperSet
modified structure SpectralMap
modified structure CompactExhaustion
modified def Filter.cocompact
modified theorem Filter.coprodᵢ_cocompact
modified theorem exists_nhds_ne_neBot
modified def irreducibleComponents
modified theorem isClopen_biInter
modified theorem isClopen_biInter_finset
modified theorem isClopen_biUnion
modified theorem isClopen_biUnion_finset
modified theorem isClopen_iInter
modified theorem isClopen_iUnion
modified theorem isClopen_range_sigmaMk
modified theorem isCompact_iUnion
modified theorem noncompact_univ
modified theorem tsupport_mul_subset_left
modified theorem tsupport_mul_subset_right
modified theorem iInf_uniformity
modified def idRel
modified theorem toTopologicalSpace_iInf
modified theorem uniformSpace_comap_id
modified theorem CauchySeq.mem_entourage
modified theorem isComplete_iUnion_separated
modified theorem UniformSpace.Completion.ext
modified theorem equicontinuousAt_iInf_dom
modified theorem equicontinuousAt_iInf_rng
modified theorem equicontinuous_iInf_dom
modified theorem equicontinuous_iInf_rng
modified structure UniformEquiv
modified theorem Matrix.uniformContinuous
modified theorem uniformContinuous_pi
modified theorem eq_of_forall_symmetric
modified theorem eq_of_uniformity
modified theorem eq_of_uniformity_basis
modified theorem idRel_sub_separationRel
modified theorem TendstoUniformly.prod
modified theorem TendstoUniformly.prod_map
modified theorem TendstoUniformlyOn.prod
modified theorem TendstoUniformlyOn.prod_map
modified theorem UniformCauchySeqOn.comp
modified theorem UniformCauchySeqOn.prod'
modified theorem UniformCauchySeqOn.prod
modified theorem UniformCauchySeqOn.prod_map
modified def UniformFun
modified def UniformOnFun
modified theorem Equiv.uniformEmbedding
modified theorem UniformEmbedding.prod
modified theorem UniformInducing.prod
modified theorem uniformEmbedding_comap
modified structure Urysohns.CU
modified structure VectorBundleCore