Theorem Submodule.annihilator_map_mkQ_eq_colon

Modification history

2026-01-16 14:47

Mathlib/RingTheory/Ideal/Colon.lean

feat(RingTheory/Ideal): generalize Submodule.colon to sets (#33390) …

Modified Submodule.annihilator_map_mkQ_eq_colon View on Github →

2024-12-31 21:01

Mathlib/RingTheory/Ideal/Colon.lean

chore(RingTheory/Ideal/Colon): generalize to semiring (#18595) …

Added Submodule.annihilator_map_mkQ_eq_colon View on Github →