Theorems · Theorem · number theory
Nat.find.congr_simp
∀ {p p_1 : ℕ → Prop} (e_p : p = p_1) {inst : DecidablePred p} [inst_1 : DecidablePred p_1] (H : ∃ n, p n),
Nat.find H = Nat.find ⋯- Defined in
- Mathlib.Data.Nat.Find
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses Quot.sound
- Assumes
- DecidablePred
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Nat.findstatement and proof · cited by 139
Cited by11
Results whose statement or proof uses this declaration.
- emultiplicity_le_emultiplicity_iffproof · cited by 7
- Nat.sInf_eq_zeroproof · cited by 6
- PiNat.firstDiff_commproof · cited by 4
- Pell.IsFundamental.exists_of_not_isSquareproof · cited by 2
- YoungDiagram.rowLen_transposeproof · cited by 2
- Associates.count_factors_eq_find_of_dvd_powproof · cited by 1
- YoungDiagram.rowLen_ofRowLensproof · cited by 1
- JacobsonNoether.exists_separable_and_not_isCentralproof · cited by 1
- YoungDiagram.rowLens_length_ofRowLensproof · cited by 1
- YoungDiagram.colLen_transposeproof · cited by 0
- UniformSpace.metrizable_uniformityproof · cited by 0