mathlib

20cf3ca0 - feat(ring_theory/discriminant): add discr_eq_discr_of_to_matrix_coeff_is_integral (#11994)

feat(ring_theory/discriminant): add discr_eq_discr_of_to_matrix_coeff_is_integral (#11994) We add `discr_eq_discr_of_to_matrix_coeff_is_integral`: if `b` and `b'` are `ℚ`-basis of a number field `K` such that `∀ i j, is_integral ℤ (b.to_matrix b' i j)` and `∀ i j, is_integral ℤ (b'.to_matrix b i j` then `discr ℚ b = discr ℚ b'`.