Theorems · Definition · number theory
AlgHom.IsArithFrobAt.restrict
{R : Type u_1} →
{S : Type u_2} →
[inst : CommRing R] →
[inst_1 : CommRing S] →
[inst_2 : Algebra R S] →
{φ : S →ₐ[R] S} → {Q : Ideal S} → φ.IsArithFrobAt Q → S ⧸ Q →ₐ[R ⧸ Ideal.under R Q] S ⧸ QA Frobenius element at Q restricts to the Frobenius map on S ⧸ Q.
- Defined in
- Mathlib.RingTheory.Frobenius
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 100 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Algebrastatement and proof · cited by 11,388
- RingHomproof · cited by 10,189
- Idealstatement and proof · cited by 4,748
- AlgHomstatement and proof · cited by 3,236
- HasQuotient.Quotientstatement and proof · cited by 2,301
- RingHomClass.toRingHomproof · cited by 746
- Ideal.understatement and proof · cited by 170
- Ideal.quotientMapproof · cited by 27
- AlgHom.IsArithFrobAtstatement and proof · cited by 13
- AlgHom.IsArithFrobAt.le_comapproof · cited by 1
Cited by5
Results whose statement or proof uses this declaration.
- AlgHom.IsArithFrobAt.comap_eqproof · cited by 2
- AlgHom.IsArithFrobAt.restrict_applystatement · cited by 1
- AlgHom.IsArithFrobAt.restrict_injectivestatement and proof · cited by 1
- AlgHom.IsArithFrobAt.restrict_mkstatement · cited by 1
- AlgHom.IsArithFrobAt.restrict.congr_simpstatement and proof · cited by 0