Commit 2024-07-31 01:05 876ccfb5

View on Github →

chore: backports for leanprover/lean4#4814 (part 7) (#15332) see https://github.com/leanprover-community/mathlib4/pull/15245

Estimated changes

Modified Mathlib/Algebra/Module/LinearMap/Defs.lean

modified theorem IsLinearMap.map_neg

modified theorem IsLinearMap.map_sub

modified theorem IsLinearMap.map_zero

modified def IsLinearMap.mk'

modified theorem IsLinearMap.mk'_apply

Modified Mathlib/Algebra/Order/Group/PosPart.lean

Modified Mathlib/Data/Set/Lattice.lean

Modified Mathlib/Order/Interval/Set/OrdConnectedComponent.lean

Modified Mathlib/SetTheory/ZFC/Basic.lean

modified theorem ZFSet.choice_isFunc

modified theorem ZFSet.choice_mem

modified theorem ZFSet.choice_mem_aux