Find

📁 Source: Mathlib/Data/Nat/Find.lean

Statistics

Metric	Count
Definitions `find`, `findGreatest`, `findX`	3
Theorems `findGreatest_eq`, `findGreatest_eq_iff`, `findGreatest_eq_zero_iff`, `findGreatest_is_greatest`, `findGreatest_le`, `findGreatest_mono`, `findGreatest_mono_left`, `findGreatest_mono_right`, `findGreatest_of_ne_zero`, `findGreatest_of_not`, `findGreatest_pos`, `findGreatest_spec`, `findGreatest_succ`, `findGreatest_zero`, `find_add`, `find_comp_succ`, `find_congr`, `find_congr'`, `find_eq_iff`, `find_eq_zero`, `find_le`, `find_le_iff`, `find_lt_iff`, `find_min`, `find_min'`, `find_mono`, `find_mono_of_le`, `find_pos`, `find_spec`, `le_findGreatest`, `le_find_iff`, `lt_find_iff`	32
Total	35

Nat

Definitions

Name	Category	Theorems
`find` 📖	CompOp	42 math math: `sSup_def`, `PiNat.firstDiff_def`, `find_lt_iff`, `find_mono_of_le`, `least_ascending_central_series_length_eq_nilpotencyClass`, `Polynomial.rootMultiplicity_eq_natFind_of_ne_zero`, `Polynomial.rootMultiplicity_eq_nat_find_of_nonzero`, `least_descending_central_series_length_eq_nilpotencyClass`, `Ideal.ramificationIdx_eq_find`, `le_find_iff`, `find_le`, `Part.fix_def`, `PartENat.find_get`, `toZ_of_ge`, `find_comp_succ`, `sInf_def`, `find_eq_zero`, `nth_zero_of_exists`, `Set.Nonempty.isLeast_natFind`, `Measurable.find`, `find_le_iff`, `find_pos`, `LieModule.chainTopCoeff_add_one`, `Associates.count_factors_eq_find_of_dvd_pow`, `find_min'`, `Fin.find_nat_lt`, `Subtype.coe_bot`, `find_mono`, `Associates.eq_pow_find_of_dvd_irreducible_pow`, `FormalMultilinearSeries.order_eq_find'`, `FormalMultilinearSeries.order_eq_find`, `lt_find_iff`, `Fin.val_find`, `find_congr`, `find_congr'`, `preimage_find_eq_disjointed`, `isLeast_find`, `lowerCentralSeries_length_eq_nilpotencyClass`, `measurable_find`, `find_eq_iff`, `toZ_of_lt`, `find_spec`
`findGreatest` 📖	CompOp	16 math math: `findGreatest_pos`, `findGreatest_of_not`, `findGreatest_spec`, `findGreatest_zero`, `le_findGreatest`, `findGreatest_mono`, `Set.finite_range_findGreatest`, `findGreatest_eq_zero_iff`, `findGreatest_eq`, `measurable_findGreatest`, `Primrec.nat_findGreatest`, `findGreatest_succ`, `findGreatest_mono_left`, `findGreatest_eq_iff`, `findGreatest_le`, `findGreatest_mono_right`
`findX` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`findGreatest_eq` 📖	mathematical	—	`findGreatest`	—	—
`findGreatest_eq_iff` 📖	mathematical	—	`findGreatest`	—	`findGreatest_zero` `findGreatest_eq` `le_refl` `Decidable.lt_or_eq_of_le` `findGreatest_of_not`
`findGreatest_eq_zero_iff` 📖	mathematical	—	`findGreatest`	—	—
`findGreatest_is_greatest` 📖	—	`findGreatest`	—	—	`findGreatest_eq_iff`
`findGreatest_le` 📖	mathematical	—	`findGreatest`	—	`findGreatest_eq_iff`
`findGreatest_mono` 📖	mathematical	—	`findGreatest`	—	`le_trans` `findGreatest_mono_right` `findGreatest_mono_left`
`findGreatest_mono_left` 📖	mathematical	—	`findGreatest`	—	`le_refl` `findGreatest_eq` `findGreatest_of_not` `le_trans` `findGreatest_mono_right`
`findGreatest_mono_right` 📖	mathematical	—	`findGreatest`	—	`findGreatest_succ` `le_trans` `findGreatest_le`
`findGreatest_of_ne_zero` 📖	—	`findGreatest`	—	—	`findGreatest_eq_iff`
`findGreatest_of_not` 📖	mathematical	—	`findGreatest`	—	—
`findGreatest_pos` 📖	mathematical	—	`findGreatest`	—	`findGreatest_eq_zero_iff` `Mathlib.Tactic.Push.not_forall_eq`
`findGreatest_spec` 📖	mathematical	—	`findGreatest`	—	`findGreatest_eq_zero_iff` `findGreatest_eq_iff`
`findGreatest_succ` 📖	mathematical	—	`findGreatest`	—	—
`findGreatest_zero` 📖	mathematical	—	`findGreatest`	—	—
`find_add` 📖	—	`find`	—	—	`le_antisymm` `le_find_iff` `le_trans` `find_le`
`find_comp_succ` 📖	mathematical	—	`find`	—	`find_eq_iff` `find_spec` `find_min`
`find_congr` 📖	mathematical	—	`find`	—	`le_antisymm` `le_rfl` `find_mono_of_le`
`find_congr'` 📖	mathematical	—	`find`	—	`find_congr`
`find_eq_iff` 📖	mathematical	—	`find`	—	`find_min'`
`find_eq_zero` 📖	mathematical	—	`find`	—	—
`find_le` 📖	mathematical	—	`find`	—	`find_le_iff` `le_refl`
`find_le_iff` 📖	mathematical	—	`find`	—	—
`find_lt_iff` 📖	mathematical	—	`find`	—	`find_spec` `find_min'`
`find_min` 📖	—	`find`	—	—	—
`find_min'` 📖	mathematical	—	`find`	—	`find_min`
`find_mono` 📖	mathematical	—	`find`	—	`find_mono_of_le`
`find_mono_of_le` 📖	mathematical	—	`find`	—	`find_min'` `le_rfl` `find_spec`
`find_pos` 📖	mathematical	—	`find`	—	`Iff.not` `find_eq_zero`
`find_spec` 📖	mathematical	—	`find`	—	—
`le_findGreatest` 📖	mathematical	—	`findGreatest`	—	`le_of_not_gt` `findGreatest_eq_iff`
`le_find_iff` 📖	mathematical	—	`find`	—	—
`lt_find_iff` 📖	mathematical	—	`find`	—	—

---

← Back to Index