Commit 2023-07-15 18:30 4dcc0e11

View on Github →

refactor: use SemilinearMapClass in LinearMap.eqLocus (#5929) Also prove extensionality on a codisjoint pair of submodules.

Estimated changes

Modified Mathlib/LinearAlgebra/Basic.lean

modified def LinearMap.eqLocus

modified theorem LinearMap.eqLocus_eq_ker_sub

added theorem LinearMap.eqLocus_eq_top

modified theorem LinearMap.eqLocus_same

modified theorem LinearMap.eqLocus_toAddSubmonoid

added theorem LinearMap.eqOn_sup

added theorem LinearMap.ext_on_codisjoint

added theorem LinearMap.le_eqLocus

modified theorem LinearMap.mem_eqLocus

Modified Mathlib/LinearAlgebra/Span.lean

modified theorem LinearMap.eqOn_span'

modified theorem LinearMap.eqOn_span

added theorem LinearMap.eqOn_span_iff

modified theorem LinearMap.ext_on

modified theorem LinearMap.ext_on_range