Commit 2024-08-12 18:29 ef99038f

View on Github →

chore: move to v4.11.0-rc2 (new variable command) (#15726)

Estimated changes

modified theorem Prime.dvd_of_dvd_pow
modified theorem Prime.dvd_or_dvd
modified theorem Prime.isPrimal
modified def Submonoid.giMapComap
modified theorem map_dvd_iff
modified theorem norm_zsmul
modified theorem PicardLindelof.exists_fixed
modified theorem Turing.TM1to1.tr_respects
modified theorem EquivLike.subsingleton_dom
modified theorem Real.IsConjExponent.conj_eq
modified theorem IsGroupHom.comp
modified theorem IsGroupHom.injective_iff
modified theorem IsGroupHom.map_div
modified theorem IsGroupHom.map_inv
modified theorem IsMonoidHom.map_mul'
modified theorem Matrix.Represents.eq
modified theorem LinearMap.lsum_apply
modified theorem dite_prop_iff_and
modified theorem dite_prop_iff_or
modified theorem MeasureTheory.aecover_Icc
modified theorem MeasureTheory.aecover_Ici
modified theorem MeasureTheory.aecover_Iic
modified theorem torusIntegral_dim0
modified theorem torusIntegral_succ
modified theorem torusIntegral_succAbove
modified theorem Dioph.pow_dioph
modified theorem ZMod.exists_sq_eq_two_iff
modified theorem legendreSym.at_neg_two
modified theorem legendreSym.at_two
modified theorem PadicInt.lift_self
modified theorem PythagoreanTriple.eq
modified theorem PythagoreanTriple.mul
modified theorem PythagoreanTriple.symm
modified theorem GaloisConnection.l_sSup
modified theorem GaloisConnection.l_sup
modified theorem GaloisConnection.lt_iff_lt
modified theorem GaloisConnection.u_eq
modified theorem GaloisConnection.u_inf
deleted theorem AlgHom.coe_ideal_map
deleted theorem AlgHom.coe_ker
deleted def Algebra.idealMap
added theorem Ideal.AlgHom.coe_ker
added theorem Ideal.Ideal.map_sInf
added theorem Ideal.RingHom.ker_eq
added theorem Ideal.RingHom.mem_ker
modified theorem Ideal.coe_comap
modified def Ideal.comap
modified theorem Ideal.comap_mono
modified theorem Ideal.comap_ne_top
deleted theorem Ideal.ker_le_comap
modified theorem Ideal.map_le_iff_le_comap
deleted theorem Ideal.map_sInf
modified theorem Ideal.mem_comap
deleted theorem RingHom.comap_ker
deleted def RingHom.ker
deleted theorem RingHom.ker_coe_equiv
deleted theorem RingHom.ker_eq
deleted theorem RingHom.ker_eq_comap_bot
deleted theorem RingHom.ker_equiv
deleted theorem RingHom.ker_isPrime
deleted theorem RingHom.ker_ne_top
deleted theorem RingHom.ker_rangeRestrict
deleted theorem RingHom.mem_ker
deleted theorem RingHom.not_one_mem_ker
deleted theorem RingHom.sub_mem_ker_iff
modified theorem Ideal.map_eq_top_iff
modified theorem IsLocalization.at_units
modified theorem IsLocalization.eq_iff_eq
modified theorem IsLocalization.map_comap
modified def Tilt
modified theorem FiniteDimensional.complete
modified theorem closedEmbedding_smul_left
modified theorem isClosedMap_smul_left
modified theorem tendsto_div_comap_self
modified theorem IsSeparatedMap.comp_left
modified theorem IsClosed.HasSeparatingCover
modified theorem Set.Finite.isGδ
modified structure ConHom
modified structure LinHom
modified theorem add_Con'
modified theorem add_Con
modified theorem add_Lin'
modified theorem add_Lin
modified def foo3