Mathlib Map

Theorems · Theorem · number theory

FiniteField.Extension.congr_simp

∀ (k : Type u_1) [inst : Field k] (p p_1 : ℕ) (e_p : p = p_1) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP k p]
  (n n_1 : ℕ), n = n_1 → FiniteField.Extension k p n = FiniteField.Extension k p_1 n_1
Defined in
Mathlib.FieldTheory.Finite.Extension
Cited by
0 results in Mathlib
Foundations
Depth 136 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
FieldFactCharP
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Field · cited by 7404FieldFact · cited by 2726FactNat.Prime · cited by 2059Nat.PrimeCharP · cited by 478CharPFiniteField.Extension · cited by 13FiniteField.ExtensionExtension.congr_simpCITED BYCITES

Cites5

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

  • Fieldstatement and proof · cited by 7,404
  • Factstatement and proof · cited by 2,726
  • Nat.Primestatement and proof · cited by 2,059
  • CharPstatement and proof · cited by 478
  • FiniteField.Extensionstatement and proof · cited by 13

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.