Commit 2025-07-23 19:36 d3c295b4

View on Github →

style(RingTheory/IsAdjoinRoot): improve style and golf (#27374)

Factor out repeated hypotheses into variable
Golf a bunch of proofs
Remove outdated porting notes

Estimated changes

Modified Mathlib/RingTheory/IsAdjoinRoot.lean

modified theorem AdjoinRoot.isAdjoinRoot_map_eq_mk

modified def IsAdjoinRoot.aequiv

modified theorem IsAdjoinRoot.aequiv_aequiv

modified theorem IsAdjoinRoot.aequiv_map

modified theorem IsAdjoinRoot.aequiv_ofEquiv

modified theorem IsAdjoinRoot.aequiv_root

modified theorem IsAdjoinRoot.aequiv_self

modified theorem IsAdjoinRoot.aequiv_symm

modified theorem IsAdjoinRoot.aequiv_trans

modified theorem IsAdjoinRoot.aeval_eq

modified theorem IsAdjoinRoot.aeval_root

modified theorem IsAdjoinRoot.algebraMap_apply

modified theorem IsAdjoinRoot.apply_eq_lift

modified theorem IsAdjoinRoot.coe_liftHom

modified theorem IsAdjoinRoot.eq_lift

modified theorem IsAdjoinRoot.eq_liftHom

modified theorem IsAdjoinRoot.eval₂_repr_eq_eval₂_of_map_eq

modified theorem IsAdjoinRoot.ext

modified theorem IsAdjoinRoot.ext_map

modified def IsAdjoinRoot.lift

modified def IsAdjoinRoot.liftHom

modified theorem IsAdjoinRoot.liftHom_aequiv

modified theorem IsAdjoinRoot.liftHom_map

modified theorem IsAdjoinRoot.liftHom_root

modified theorem IsAdjoinRoot.lift_aequiv

modified theorem IsAdjoinRoot.lift_algebraMap

modified theorem IsAdjoinRoot.lift_algebraMap_apply

modified theorem IsAdjoinRoot.lift_map

modified theorem IsAdjoinRoot.lift_root

modified theorem IsAdjoinRoot.lift_self

modified theorem IsAdjoinRoot.lift_self_apply

modified theorem IsAdjoinRoot.map_X

modified theorem IsAdjoinRoot.map_eq_zero_iff

modified theorem IsAdjoinRoot.map_repr

modified theorem IsAdjoinRoot.map_self

modified theorem IsAdjoinRoot.mem_ker_map

modified def IsAdjoinRoot.ofEquiv

modified theorem IsAdjoinRoot.ofEquiv_aequiv

modified theorem IsAdjoinRoot.ofEquiv_root

modified def IsAdjoinRoot.repr

modified theorem IsAdjoinRoot.repr_add_sub_repr_add_repr_mem_span

modified theorem IsAdjoinRoot.repr_zero_mem_span

modified def IsAdjoinRoot.root

modified theorem IsAdjoinRoot.subsingleton

modified def IsAdjoinRootMonic.basis

modified theorem IsAdjoinRootMonic.basis_apply

modified theorem IsAdjoinRootMonic.basis_one

modified theorem IsAdjoinRootMonic.basis_repr

modified def IsAdjoinRootMonic.coeff

modified theorem IsAdjoinRootMonic.coeff_algebraMap

modified theorem IsAdjoinRootMonic.coeff_apply

modified theorem IsAdjoinRootMonic.coeff_apply_coe

modified theorem IsAdjoinRootMonic.coeff_apply_le

modified theorem IsAdjoinRootMonic.coeff_apply_lt

modified theorem IsAdjoinRootMonic.coeff_injective

modified theorem IsAdjoinRootMonic.coeff_one

modified theorem IsAdjoinRootMonic.coeff_root

modified theorem IsAdjoinRootMonic.coeff_root_pow

modified theorem IsAdjoinRootMonic.deg_ne_zero

modified theorem IsAdjoinRootMonic.deg_pos

modified theorem IsAdjoinRootMonic.ext_elem

modified theorem IsAdjoinRootMonic.ext_elem_iff

modified theorem IsAdjoinRootMonic.isIntegral_root

modified def IsAdjoinRootMonic.liftPolyₗ

modified theorem IsAdjoinRootMonic.map_modByMonic

modified theorem IsAdjoinRootMonic.map_modByMonicHom

modified def IsAdjoinRootMonic.modByMonicHom

modified theorem IsAdjoinRootMonic.modByMonicHom_map

modified theorem IsAdjoinRootMonic.modByMonicHom_root

modified theorem IsAdjoinRootMonic.modByMonicHom_root_pow

modified theorem IsAdjoinRootMonic.modByMonic_repr_map

modified def IsAdjoinRootMonic.powerBasis