Commit 2025-03-03 14:53 6cecf71a

View on Github →

chore: bump toolchain to v4.18.0-rc1 (#22500) This PR merges bump/v4.18.0 into master.

Estimated changes

modified structure Subalgebra
modified theorem FreeMonoid.length_eq_zero
modified structure Submodule
modified structure NonUnitalStarSubsemiring
modified structure SubStarSemigroup
modified structure StarSubsemiring
modified structure AlgebraicGeometry.Scheme.Hom
modified structure NormedSpace.Core
modified structure CategoryTheory.Functor
modified structure CategoryTheory.BicartesianSq
modified structure CategoryTheory.IsPullback
modified structure CategoryTheory.IsPushout
modified structure SimpleGraph.Walk.IsCircuit
modified structure SimpleGraph.Walk.IsCycle
modified structure SimpleGraph.Walk.IsPath
deleted theorem Computable.list_get?
deleted theorem Primrec.list_get?
deleted theorem Primrec.list_get?₁
modified theorem Primrec.list_getElem?
deleted theorem Array.extract_append_left
deleted theorem Array.extract_extract
deleted theorem Fin.mk_eq_zero
deleted theorem Fin.zero_eq_mk
deleted theorem Int.toNat_of_nonpos
deleted theorem Int.toNat_eq_zero
modified theorem List.get_attach
modified theorem List.TFAE.out
modified theorem Nat.one_le_pow
deleted theorem Nat.succ_div
deleted theorem Nat.succ_div_of_dvd
deleted theorem Nat.succ_div_of_not_dvd
deleted theorem Option.pmap_map
deleted theorem Stream'.Seq.ofList_get
deleted theorem Stream'.get?_take
deleted theorem Stream'.get?_take_succ
added theorem Stream'.getElem?_take
deleted theorem String.leftpad_length
added theorem String.length_leftpad
modified theorem $typeName.intCast_def
modified theorem $typeName.natCast_def
modified theorem $typeName.neg_def
modified theorem $typeName.nsmul_def
modified theorem $typeName.pow_def
modified theorem $typeName.val_injective
modified theorem $typeName.zsmul_def
modified structure CircleDeg1Lift
modified structure MeasureTheory.Conservative
modified structure Ergodic
modified structure QuasiErgodic
modified structure EckmannHilton.IsUnital
modified structure HNNExtension.NormalWord
deleted def Lean.Expr.fvarId?
modified structure Filter.HasAntitoneBasis
modified structure Filter.IsAntitoneBasis
modified structure Filter.HasCountableBasis
modified structure Filter.IsCountableBasis
modified structure CompleteOrthogonalIdempotents
modified structure RingTheory.Sequence.IsRegular
modified structure Linarith.GlobalPreprocessor
modified structure Linarith.Preprocessor
modified structure AddGroupTopology
modified structure GroupTopology
modified structure RingTopology
modified structure CocompactMap
modified structure Topology.IsClosedEmbedding
modified structure Topology.IsEmbedding
modified structure Topology.IsOpenEmbedding
modified structure IsDenseEmbedding
modified structure IsDenseInducing
deleted theorem Vector.tendsto_cons
deleted theorem Vector.tendsto_insertIdx
modified structure IsProperMap
modified structure IsSpectralMap
modified structure IsUniformEmbedding
modified structure UnderScoreDigit.Prod2
modified structure UnderScoreDigit.Prod3
modified def databases