Commit 2025-08-18 07:35 55affb06

View on Github →

doc: some missing docstrings (#28585)

Estimated changes

Modified Mathlib/Algebra/Algebra/Hom.lean

Modified Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

Modified Mathlib/Algebra/MonoidAlgebra/MapDomain.lean

Modified Mathlib/Algebra/Polynomial/Basic.lean

Modified Mathlib/Analysis/Distribution/SchwartzSpace.lean

Modified Mathlib/Analysis/Normed/Operator/Banach.lean

Modified Mathlib/GroupTheory/Perm/Cycle/Concrete.lean

Modified Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean

Modified Mathlib/LinearAlgebra/AffineSpace/Basis.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

Modified Mathlib/Logic/Equiv/Defs.lean

Modified Mathlib/MeasureTheory/Measure/Stieltjes.lean

Modified Mathlib/NumberTheory/ModularForms/SlashInvariantForms.lean

Modified Mathlib/Order/Atoms.lean

Modified Mathlib/Order/Filter/Germ/Basic.lean

modified def Filter.Germ.ofFun

Modified Mathlib/Topology/Homotopy/Equiv.lean

Modified Mathlib/Topology/MetricSpace/Dilation.lean

Modified scripts/nolints.json