Theorems · Theorem · commutative algebra

Algebra.FiniteType.of_surjective

∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [Algebra.FiniteType R A] (f : A →ₐ[R] B),
  Function.Surjective ⇑f → Algebra.FiniteType R B

Defined in

Mathlib.RingTheory.FiniteType

Cited by

11 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringSemiringSemiringAlgebraAlgebraAlgebra.FiniteType