Commit 2025-07-04 15:43 241db1e2

View on Github →

chore: remove unnecessary noncomputable attributes after 4.22.0 rc3 (#26751) These were likely all fixed due to leanprover/lean4#8691.

Estimated changes

Modified Mathlib/AlgebraicGeometry/IdealSheaf/Basic.lean

added def AlgebraicGeometry.Scheme.kerFunctor

Modified Mathlib/AlgebraicGeometry/Morphisms/Etale.lean

added def AlgebraicGeometry.Scheme.Etale.forget

added def AlgebraicGeometry.Scheme.Etale.forgetFullyFaithful

Modified Mathlib/NumberTheory/LSeries/Nonvanishing.lean

added def DirichletCharacter.zetaMul

Modified Mathlib/Probability/ProbabilityMassFunction/Binomial.lean

added def PMF.binomial

Modified Mathlib/Topology/ContinuousMap/Bounded/Basic.lean