Theorems · Definition · ring theory

AlgEquiv.funUnique

(R : Type u_3) →
  (ι : Type u_4) →
    [inst : CommSemiring R] →
      (S : Type u_8) → [inst_1 : Semiring S] → [inst_2 : Algebra R S] → [Unique ι] → (ι → S) ≃ₐ[R] S

If ι has a unique element, then ι → S is isomorphic to S as an R-algebra.

Defined in: Mathlib.Algebra.Algebra.Pi
Cited by: 3 results in Mathlib
Foundations: Depth 22 from the axioms · uses propext, Quot.sound
Assumes: CommSemiring Semiring Algebra Unique

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Semiringstatement and proof · cited by 13,802
Algebrastatement and proof · cited by 11,388
CommSemiringstatement and proof · cited by 10,911
AlgEquivstatement · cited by 1,681
Uniquestatement and proof · cited by 400
AlgEquiv.ofRingEquivproof · cited by 12

Cited by3

Results whose statement or proof uses this declaration.

AlgEquiv.funUnique_applystatement · cited by 0
AlgEquiv.funUnique_symm_applystatement · cited by 0
Algebra.IsFiniteSplit.exists_tensorProduct_of_etaleproof · cited by 0