Commit 2024-11-09 15:00 19236650

View on Github →

feat(RingTheory/Algebraic): add Algebra.IsAlgebraic.[of_]ringHom_of_comp_eq and iff version (#18769) ... parallel to element-wise IsAlgebraic.[of_]ringHom_of_comp_eq.

Estimated changes

Modified Mathlib/RingTheory/Algebraic.lean

added theorem Algebra.IsAlgebraic.of_ringHom_of_comp_eq

added theorem Algebra.IsAlgebraic.ringHom_of_comp_eq

modified theorem IsAlgebraic.of_ringHom_of_comp_eq

added theorem IsAlgebraic.ringHom_of_comp_eq

added theorem algebra_isAlgebraic_ringHom_iff_of_comp_eq

modified theorem isAlgebraic_ringHom_iff_of_comp_eq