Def LinearMap.reduceModIdeal

Modification history

2026-08-17 11:47

Mathlib/RingTheory/AdicCompletion/Functoriality.lean

chore(RingTheory/AdicCompletion): make `AdicCompletion.map` linear on linear maps (#38324) …

Modified LinearMap.reduceModIdeal View on Github →

2024-06-11 14:59

Mathlib/RingTheory/AdicCompletion/Functoriality.lean

feat(RingTheory/AdicCompletion): functoriality (#12543) …

Added LinearMap.reduceModIdeal View on Github →