Commit 2023-06-22 20:41 347389b4

View on Github →

feat: port RingTheory.Discriminant (#5374)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Discriminant.lean

added theorem Algebra.discr_def

added theorem Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two

added theorem Algebra.discr_eq_discr_of_toMatrix_coeff_isIntegral

added theorem Algebra.discr_isIntegral

added theorem Algebra.discr_isUnit_of_basis

added theorem Algebra.discr_mul_isIntegral_mem_adjoin

added theorem Algebra.discr_not_zero_of_basis

added theorem Algebra.discr_of_matrix_mulVec

added theorem Algebra.discr_of_matrix_vecMul

added theorem Algebra.discr_powerBasis_eq_norm

added theorem Algebra.discr_powerBasis_eq_prod''

added theorem Algebra.discr_powerBasis_eq_prod'

added theorem Algebra.discr_powerBasis_eq_prod

added theorem Algebra.discr_reindex

added theorem Algebra.discr_zero_of_not_linearIndependent