Commit 2025-07-28 08:17 4c7a21bb

View on Github →

chore(LinearAlgebra/Matrix/Ideal): deprecate matricesOver (#27575) Ideal.matricesOver is not an ideal name - one should use matrix instead of matricesOver, see also #27190 where the analogous Set.matrix, Subring.matrix, etc are defined. Zulip thread

Estimated changes

deleted def Ideal.matricesOver
deleted theorem Ideal.matricesOver_bot
deleted theorem Ideal.matricesOver_top
added def Ideal.matrix
added theorem Ideal.matrix_bot
added theorem Ideal.matrix_monotone
added theorem Ideal.matrix_top
deleted theorem Ideal.mem_matricesOver
added theorem Ideal.mem_matrix