Theorems · Definition · ring theory
AlgEquiv.ofRingEquiv
{R : Type uR} →
{A₁ : Type uA₁} →
{A₂ : Type uA₂} →
[inst : CommSemiring R] →
[inst_1 : Semiring A₁] →
[inst_2 : Semiring A₂] →
[inst_3 : Algebra R A₁] →
[inst_4 : Algebra R A₂] →
{f : A₁ ≃+* A₂} → (∀ (x : R), f ((algebraMap R A₁) x) = (algebraMap R A₂) x) → A₁ ≃ₐ[R] A₂Promotes a linear RingEquiv to an AlgEquiv.
- Defined in
- Mathlib.Algebra.Algebra.Equiv
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Semiringstatement and proof · cited by 13,802
- Algebrastatement and proof · cited by 11,388
- CommSemiringstatement and proof · cited by 10,911
- RingHomstatement · cited by 10,189
- Algebra.algebraMapstatement and proof · cited by 4,706
- AlgEquivstatement · cited by 1,681
- RingEquivstatement and proof · cited by 1,147
- RingEquiv.symmproof · cited by 567
Cited by26
Results whose statement or proof uses this declaration.
- DoubleQuot.quotQuotEquivQuotOfLEₐproof · cited by 8
- PowerBasis.quotientEquivQuotientMinpolyMapproof · cited by 5
- AlgCat.intEquivalenceproof · cited by 5
- AdjoinRoot.quotEquivQuotMapproof · cited by 5
- AlgEquiv.prodCongrproof · cited by 4
- DoubleQuot.quotQuotEquivQuotSupₐproof · cited by 4
- RingHom.finiteType_respectsIsoproof · cited by 4
- AlgCat.restrictScalarsComp'proof · cited by 4
- AlgCat.restrictScalarsId'proof · cited by 4
- DoubleQuot.quotQuotEquivCommₐproof · cited by 4
- AlgEquiv.funUniqueproof · cited by 3
- IsIntegrallyClosed.of_equivproof · cited by 3