Commit 2026-08-17 11:47 5ed84203

View on Github →

chore(RingTheory/AdicCompletion): make AdicCompletion.map linear on linear maps (#38324) This PR upgrades AdicCompletion.map to be an R-linear map on the space of linear maps M →ₗ[R] N.

Estimated changes

Modified Mathlib/RingTheory/AdicCompletion/Basic.lean

added theorem AdicCompletion.lift_add

added theorem AdicCompletion.lift_smul

Modified Mathlib/RingTheory/AdicCompletion/Functoriality.lean

modified def AdicCompletion.map

modified def LinearMap.reduceModIdeal