Commit 2024-10-17 08:31 9800ff6d

View on Github →

feat(LinearAlgebra/Matrix): characterize ideals in matrix rings (#17750)

Define left and two-sided ideals in a matrix ring.
Show that two-sided matrix ideals are order-isomorphic to two-sided ideals in the base ring. This code is taken from FLT, from here.

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Matrix/Ideal.lean

added def Ideal.matricesOver

added theorem Ideal.matricesOver_bot

added theorem Ideal.matricesOver_monotone

added theorem Ideal.matricesOver_strictMono_of_nonempty

added theorem Ideal.matricesOver_top

added theorem Ideal.mem_matricesOver

added theorem TwoSidedIdeal.asIdeal_matricesOver

added def TwoSidedIdeal.equivMatricesOver

added def TwoSidedIdeal.matricesOver

added theorem TwoSidedIdeal.matricesOver_bot

added theorem TwoSidedIdeal.matricesOver_monotone

added theorem TwoSidedIdeal.matricesOver_strictMono_of_nonempty

added theorem TwoSidedIdeal.matricesOver_top

added theorem TwoSidedIdeal.mem_matricesOver

added def TwoSidedIdeal.orderIsoMatricesOver