Commit 2025-05-17 15:42 5decab90

View on Github →

feat(LinearAlgebra/Matrix): num and denom of a rational matrix (#24951) Write a rational matrix as an integer matrix Matrix.num divided by a nonzero natural Matrix.den.

Estimated changes

added theorem Matrix.den_dvd_iff
added theorem Matrix.den_intCast
added theorem Matrix.den_map_intCast
added theorem Matrix.den_map_natCast
added theorem Matrix.den_natCast
added theorem Matrix.den_ne_zero
added theorem Matrix.den_neg
added theorem Matrix.den_ofNat
added theorem Matrix.den_one
added theorem Matrix.den_transpose
added theorem Matrix.den_zero
added theorem Matrix.map_mul_intCast
added theorem Matrix.map_mul_natCast
added theorem Matrix.map_mul_ratCast
added theorem Matrix.num_div_den
added theorem Matrix.num_eq_zero_iff
added theorem Matrix.num_intCast
added theorem Matrix.num_map_intCast
added theorem Matrix.num_map_natCast
added theorem Matrix.num_natCast
added theorem Matrix.num_neg
added theorem Matrix.num_ofNat
added theorem Matrix.num_one
added theorem Matrix.num_transpose
added theorem Matrix.num_zero