Theorems · Definition · ring theory
AlgEquiv.refl
{R : Type uR} →
{A₁ : Type uA₁} → [inst : CommSemiring R] → [inst_1 : Semiring A₁] → [inst_2 : Algebra R A₁] → A₁ ≃ₐ[R] A₁Algebra equivalences are reflexive.
- Defined in
- Mathlib.Algebra.Algebra.Equiv
- Cited by
- 50 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses no axioms
- Assumes
- CommSemiringSemiringAlgebra
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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
- RingEquivproof · cited by 1,147
- RingEquiv.toEquivproof · cited by 101
- RingEquiv.reflproof · cited by 72
Cited by64
Results whose statement or proof uses this declaration.
- ContinuousAlgEquiv.reflproof · cited by 31
- Ideal.quotientEquivAlgOfEqproof · cited by 23
- Algebra.QuasiFinite.transproof · cited by 8
- Module.Finite.of_quasiFiniteproof · cited by 7
- AlgEquiv.opCommproof · cited by 5
- Ideal.fiberIsoOfBijectiveResidueFieldproof · cited by 5
- AdjoinRoot.algEquivOfAssociatedproof · cited by 4
- RingCon.comapQuotientEquivRangeₐproof · cited by 4
- IsPrimitiveRoot.norm_pow_sub_one_of_prime_pow_ne_twoproof · cited by 4
- PrimeSpectrum.mem_image_comap_basicOpenproof · cited by 3
- Algebra.TensorProduct.leftCommproof · cited by 3
- Algebra.WeaklyQuasiFiniteAt.baseChangeproof · cited by 2