Commit 2025-01-22 10:59 e9495448

View on Github →

chore(AssociatedPrime): use ker toSpanSingleton instead of annihilator span singleton (#20155) Maybe better in terms of defeq, not sure if this is really an improvement.

Estimated changes

Modified Mathlib/LinearAlgebra/Span/Basic.lean

added theorem LinearMap.toSpanSingleton_eq_zero_iff

added theorem LinearMap.toSpanSingleton_injective

Modified Mathlib/RingTheory/Ideal/AssociatedPrime.lean

Modified Mathlib/RingTheory/Ideal/Maps.lean

added theorem Ideal.Submodule.annihilator_span

added theorem Ideal.Submodule.annihilator_span_singleton