Theorem Algebra.adjoin_algebraMap

Modification history

2023-08-23 11:25

Mathlib/RingTheory/Adjoin/Basic.lean

feat(RingTheory/FiniteType): generalize some results to non-commutative rings (#6681) …

Modified Algebra.adjoin_algebraMap View on Github →

2023-04-02 14:13

Mathlib/RingTheory/Adjoin/Tower.lean

feat: port RingTheory.Adjoin.Tower (#3210)

Added Algebra.adjoin_algebraMap View on Github →