mod

📁 Source: MathlibTest/GCongr/mod.lean

Statistics

Metric	Count
Definitions mod, mod, mod, mod, mod, mod, mod	7
Theorems mod, mod	2
Total	9

CategoryTheory.Mod_

Definitions

Name	Category	Theorems
mod 📖	CompOp	6 math math: comap_obj_mod, comap_map_hom, Hom.isMod_Hom, regular_mod_smul, assoc_flip, trivialAction_mod_smul

Function.IsPeriodicPt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mod 📖	—	Function.IsPeriodicPt	—	—	iterate_mod_apply

Num

Definitions

Name	Category	Theorems
mod 📖	CompOp	—

Ordinal

Definitions

Name	Category	Theorems
mod 📖	CompOp	26 math math: Mathlib.Meta.NormNum.isNat_ordinalMod, mod_self, mod_le, div_add_mod, CNF_ne_zero, mul_mod, mod_one, natCast_mod, mod_lt, dvd_iff_mod_eq_zero, mul_mod_mul, mod_opow_log_lt_self, mul_add_mod_self, log_mod_opow_log_lt_log_self, CNF.rec_pos, mod_zero, CNFRec_pos, natCast_mod_omega0, CNF.ne_zero, mod_mod, mul_add_mod_mul, mod_mod_of_dvd, mod_eq_zero_of_dvd, mod_eq_of_lt, mod_def, zero_mod

PNat

Definitions

Name	Category	Theorems
mod 📖	CompOp	7 math math: mod_coe, mod_add_div, mod_add_div', div_add_mod, dvd_iff', div_add_mod', mod_le

Polynomial

Definitions

Name	Category	Theorems
mod 📖	CompOp	—

PowerSeries.IsWeierstrassDivisorAt

Definitions

Name	Category	Theorems
mod 📖	CompOp	6 math math: mod_coe_eq_self, mod'_mk_eq_mod, mod_add, mod_smul, mod_zero, isWeierstrassDivisionAt_div_mod

ZNum

Definitions

Name	Category	Theorems
mod 📖	CompOp	—

legendreSym

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mod 📖	mathematical	—	legendreSym	—	ZMod.intCast_mod

---

← Back to Index