Commit 2023-05-23 07:30 e1328b4a

View on Github →

feat: port RingTheory.PowerBasis (#4238)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Logic/IsEmpty.lean

Created Mathlib/RingTheory/PowerBasis.lean

added theorem IsIntegral.mem_span_pow

added theorem PowerBasis.adjoin_eq_top_of_gen_mem_adjoin

added theorem PowerBasis.adjoin_gen_eq_top

added theorem PowerBasis.aeval_minpolyGen

added theorem PowerBasis.algHom_ext

added theorem PowerBasis.coe_basis

added theorem PowerBasis.constr_pow_aeval

added theorem PowerBasis.constr_pow_algebraMap

added theorem PowerBasis.constr_pow_gen

added theorem PowerBasis.constr_pow_mul

added theorem PowerBasis.degree_minpoly

added theorem PowerBasis.degree_minpolyGen

added theorem PowerBasis.dim_le_degree_of_root

added theorem PowerBasis.dim_le_natDegree_of_root

added theorem PowerBasis.dim_ne_zero

added theorem PowerBasis.dim_pos

added theorem PowerBasis.equivOfMinpoly_aeval

added theorem PowerBasis.equivOfMinpoly_gen

added theorem PowerBasis.equivOfMinpoly_map

added theorem PowerBasis.equivOfMinpoly_symm

added theorem PowerBasis.equivOfRoot_aeval

added theorem PowerBasis.equivOfRoot_gen

added theorem PowerBasis.equivOfRoot_map

added theorem PowerBasis.equivOfRoot_symm

added theorem PowerBasis.exists_eq_aeval'

added theorem PowerBasis.exists_eq_aeval

added theorem PowerBasis.finiteDimensional

added theorem PowerBasis.finrank

added theorem PowerBasis.isIntegral_gen

added theorem PowerBasis.lift_aeval

added theorem PowerBasis.lift_gen

added theorem PowerBasis.mem_span_pow'

added theorem PowerBasis.mem_span_pow

added theorem PowerBasis.minpolyGen_eq

added theorem PowerBasis.minpolyGen_map

added theorem PowerBasis.minpolyGen_monic

added theorem PowerBasis.natDegree_minpoly

added theorem PowerBasis.natDegree_minpolyGen

added structure PowerBasis

added theorem linearIndependent_pow