Commit 2025-04-18 00:22 5cffd162

View on Github →

feat: generalize TwoSidedIdeal.matricesOver to RingCon (#23641) This generalizes the result to non-associative rings, and most of results to non-unital rings.

Estimated changes

Modified Mathlib/Data/Matrix/Basis.lean

added theorem Matrix.StdBasisMatrix.stdBasisMatrix_mul_mul_stdBasisMatrix

Modified Mathlib/LinearAlgebra/Matrix/Ideal.lean

added theorem RingCon.coe_ofMatrix_eq_relationMap

added def RingCon.matrix

added theorem RingCon.matrix_apply

added theorem RingCon.matrix_apply_stdBasisMatrix

added theorem RingCon.matrix_bot

added theorem RingCon.matrix_injective

added theorem RingCon.matrix_monotone

added theorem RingCon.matrix_ofMatrix

added theorem RingCon.matrix_strictMono_of_nonempty

added theorem RingCon.matrix_top

added def RingCon.ofMatrix

added theorem RingCon.ofMatrix_matrix

added theorem RingCon.ofMatrix_rel'

added theorem RingCon.ofMatrix_rel

added theorem TwoSidedIdeal.coe_equivMatricesOver_symm_apply

modified def TwoSidedIdeal.equivMatricesOver

modified def TwoSidedIdeal.matricesOver

modified theorem TwoSidedIdeal.matricesOver_bot

modified theorem TwoSidedIdeal.matricesOver_top

modified def TwoSidedIdeal.orderIsoMatricesOver

Modified Mathlib/RingTheory/Congruence/Defs.lean

added theorem RingCon.coe_mk

Modified Mathlib/RingTheory/SimpleRing/Matrix.lean

Modified Mathlib/RingTheory/TwoSidedIdeal/Basic.lean

added theorem TwoSidedIdeal.coe_mk

added theorem TwoSidedIdeal.mem_mk