Commit 2023-05-22 18:54 7715520e

View on Github →

feat: port RingTheory.Algebraic (#4217)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Algebraic.lean

added theorem AlgEquiv.isAlgebraic

added theorem AlgEquiv.isAlgebraic_iff

added theorem AlgHom.bijective

added theorem Algebra.IsAlgebraic.algHom_bijective

added def Algebra.IsAlgebraic

added theorem Algebra.isAlgebraic_iff

added theorem Algebra.isAlgebraic_of_finite

added theorem Algebra.isAlgebraic_of_larger_base

added theorem Algebra.isAlgebraic_of_larger_base_of_injective

added theorem Algebra.isAlgebraic_trans

added theorem Algebra.isIntegral_of_finite

added def IsAlgebraic

added theorem IsIntegral.isAlgebraic

added theorem IsIntegralClosure.exists_smul_eq_mul

added theorem Polynomial.algebraMap_pi_eq_aeval

added theorem Polynomial.algebraMap_pi_self_eq_eval

added def Polynomial.hasSMulPi

added def Subalgebra.IsAlgebraic

added theorem Subalgebra.inv_mem_of_algebraic

added theorem Subalgebra.inv_mem_of_root_of_coeff_zero_ne_zero

added theorem Subalgebra.isAlgebraic_iff

added theorem Subalgebra.isField_of_algebraic

added theorem Transcendental.pow

added def Transcendental

added theorem exists_integral_multiple

added theorem inv_eq_of_aeval_divX_ne_zero

added theorem inv_eq_of_root_of_coeff_zero_ne_zero

added theorem isAlgebraic_algHom_of_isAlgebraic

added theorem isAlgebraic_algebraMap

added theorem isAlgebraic_algebraMap_iff

added theorem isAlgebraic_algebraMap_of_isAlgebraic

added theorem isAlgebraic_iff_isIntegral

added theorem isAlgebraic_iff_not_injective

added theorem isAlgebraic_int

added theorem isAlgebraic_nat

added theorem isAlgebraic_of_larger_base

added theorem isAlgebraic_of_larger_base_of_injective

added theorem isAlgebraic_of_mem_rootSet

added theorem isAlgebraic_of_pow

added theorem isAlgebraic_one

added theorem isAlgebraic_rat

added theorem isAlgebraic_zero

added theorem is_transcendental_of_subsingleton

added theorem polynomial_smul_apply'

added theorem polynomial_smul_apply