Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-04 23:34 bd7d034b

View on Github →

feat(ring_theory/nilpotent): add lemma module.End.is_nilpotent_mapq (#11831) Together with the other lemmas necessary for its proof.

Estimated changes

Modified src/linear_algebra/basic.lean

added theorem submodule.le_comap_pow_of_le_comap

Modified src/linear_algebra/quotient.lean

added theorem submodule.mapq_comp

added theorem submodule.mapq_id

added theorem submodule.mapq_pow

added theorem submodule.mapq_zero

Modified src/ring_theory/nilpotent.lean

added theorem module.End.is_nilpotent.mapq