Commit 2025-12-20 21:16 c2a50c83

View on Github →

chore: remove some backward.proofsInPublic settings (#32945)

Estimated changes

Modified Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean

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

modified def ModuleCat.Hom.hom₂

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

modified def SemimoduleCat.Hom.hom₂

Modified Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean

Modified Mathlib/Algebra/SkewMonoidAlgebra/Lift.lean

Modified Mathlib/CategoryTheory/Limits/Indization/IndObject.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean

Modified Mathlib/CategoryTheory/Presentable/IsCardinalFiltered.lean

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean

Modified Mathlib/Data/PFun.lean

Modified Mathlib/LinearAlgebra/Determinant.lean

Modified Mathlib/RingTheory/Ideal/Height.lean

Modified Mathlib/RingTheory/PicardGroup.lean

Modified Mathlib/RingTheory/Polynomial/Quotient.lean

Modified Mathlib/SetTheory/Descriptive/Tree.lean

modified def Descriptive.Tree.subAt