Commit 2023-06-19 04:18 a3b008be

View on Github →

feat: port RingTheory.IsAdjoinRoot (#5190)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/IsAdjoinRoot.lean

added theorem AdjoinRoot.isAdjoinRootMonic_map_eq_mk

added theorem AdjoinRoot.isAdjoinRootMonic_root_eq_root

added theorem AdjoinRoot.isAdjoinRoot_map_eq_mk

added theorem AdjoinRoot.isAdjoinRoot_root_eq_root

added theorem Algebra.adjoin.powerBasis'_minpoly_gen

added def IsAdjoinRoot.aequiv

added theorem IsAdjoinRoot.aequiv_aequiv

added theorem IsAdjoinRoot.aequiv_map

added theorem IsAdjoinRoot.aequiv_ofEquiv

added theorem IsAdjoinRoot.aequiv_root

added theorem IsAdjoinRoot.aequiv_self

added theorem IsAdjoinRoot.aequiv_symm

added theorem IsAdjoinRoot.aequiv_trans

added theorem IsAdjoinRoot.aeval_eq

added theorem IsAdjoinRoot.aeval_root

added theorem IsAdjoinRoot.algebraMap_apply

added theorem IsAdjoinRoot.apply_eq_lift

added theorem IsAdjoinRoot.coe_liftHom

added theorem IsAdjoinRoot.eq_lift

added theorem IsAdjoinRoot.eq_liftHom

added theorem IsAdjoinRoot.eval₂_repr_eq_eval₂_of_map_eq

added theorem IsAdjoinRoot.ext

added theorem IsAdjoinRoot.ext_map

added def IsAdjoinRoot.lift

added def IsAdjoinRoot.liftHom

added theorem IsAdjoinRoot.liftHom_aequiv

added theorem IsAdjoinRoot.liftHom_map

added theorem IsAdjoinRoot.liftHom_root

added theorem IsAdjoinRoot.lift_aequiv

added theorem IsAdjoinRoot.lift_algebraMap

added theorem IsAdjoinRoot.lift_algebraMap_apply

added theorem IsAdjoinRoot.lift_map

added theorem IsAdjoinRoot.lift_root

added theorem IsAdjoinRoot.lift_self

added theorem IsAdjoinRoot.lift_self_apply

added theorem IsAdjoinRoot.map_X

added theorem IsAdjoinRoot.map_eq_zero_iff

added theorem IsAdjoinRoot.map_repr

added theorem IsAdjoinRoot.map_self

added theorem IsAdjoinRoot.mem_ker_map

added def IsAdjoinRoot.ofEquiv

added theorem IsAdjoinRoot.ofEquiv_aequiv

added theorem IsAdjoinRoot.ofEquiv_root

added def IsAdjoinRoot.repr

added theorem IsAdjoinRoot.repr_add_sub_repr_add_repr_mem_span

added theorem IsAdjoinRoot.repr_zero_mem_span

added def IsAdjoinRoot.root

added theorem IsAdjoinRoot.subsingleton

added structure IsAdjoinRoot

added def IsAdjoinRootMonic.basis

added theorem IsAdjoinRootMonic.basis_apply

added theorem IsAdjoinRootMonic.basis_one

added theorem IsAdjoinRootMonic.basis_repr

added def IsAdjoinRootMonic.coeff

added theorem IsAdjoinRootMonic.coeff_algebraMap

added theorem IsAdjoinRootMonic.coeff_apply

added theorem IsAdjoinRootMonic.coeff_apply_coe

added theorem IsAdjoinRootMonic.coeff_apply_le

added theorem IsAdjoinRootMonic.coeff_apply_lt

added theorem IsAdjoinRootMonic.coeff_injective

added theorem IsAdjoinRootMonic.coeff_one

added theorem IsAdjoinRootMonic.coeff_root

added theorem IsAdjoinRootMonic.coeff_root_pow

added theorem IsAdjoinRootMonic.deg_ne_zero

added theorem IsAdjoinRootMonic.deg_pos

added theorem IsAdjoinRootMonic.ext_elem

added theorem IsAdjoinRootMonic.ext_elem_iff

added theorem IsAdjoinRootMonic.isIntegral_root

added def IsAdjoinRootMonic.liftPolyₗ

added theorem IsAdjoinRootMonic.map_modByMonic

added theorem IsAdjoinRootMonic.map_modByMonicHom

added theorem IsAdjoinRootMonic.minpoly_eq

added def IsAdjoinRootMonic.modByMonicHom

added theorem IsAdjoinRootMonic.modByMonicHom_map

added theorem IsAdjoinRootMonic.modByMonicHom_root

added theorem IsAdjoinRootMonic.modByMonicHom_root_pow

added theorem IsAdjoinRootMonic.modByMonic_repr_map

added def IsAdjoinRootMonic.powerBasis

added structure IsAdjoinRootMonic