Documentation Verification Report

Defs

📁 Source: Mathlib/Algebra/FiniteSupport/Defs.lean

Statistics

Metric	Count
Definitions `HasFiniteMulSupport`, `HasFiniteSupport`	2
Theorems `hasFiniteMulSupport_one`, `hasFiniteSupport_zero`	2
Total	4

Function

Definitions

Name	Category	Theorems
`HasFiniteMulSupport` 📖	MathDef	50 math math: `NumberField.FinitePlace.hasFiniteMulSupport_int`, `HasFiniteMulSupport.sup'`, `Ideal.hasFiniteMulSupport_coe`, `Multipliable.hasFiniteMulSupport_of_discreteTopology`, `HasFiniteMulSupport.iSup`, `HasFiniteMulSupport.fun_pow`, `mulSupport_along_fiber_finite_of_finite`, `HasFiniteMulSupport.fun_comp`, `NumberField.FinitePlace.mulSupport_finite`, `HasFiniteMulSupport.pi`, `HasFiniteMulSupport.fun_comp_of_injective`, `Multipliable.finite_mulSupport_of_discreteTopology`, `HasFiniteMulSupport.comp`, `finite_mulSupport_of_finprod_ne_one`, `HasFiniteMulSupport.div`, `Multiset.hasFiniteMulSupport_fun_pow_count`, `HasFiniteMulSupport.of_comp`, `HasFiniteMulSupport.inv`, `hasFiniteMulSupport_of_finprod_ne_one`, `HasFiniteMulSupport.fun_div`, `NumberField.FinitePlace.hasFiniteMulSupport`, `HasFiniteMulSupport.prod`, `HasFiniteMulSupport.fst`, `HasFiniteMulSupport.mul`, `finprod_def'`, `HasFiniteMulSupport.sup`, `hasFiniteMulSupport_one`, `NumberField.FinitePlace.mulSupport_finite_int`, `HasFiniteMulSupport.max`, `Height.AdmissibleAbsValues.mulSupport_finite`, `HasFiniteMulSupport.zpow`, `Ideal.finite_mulSupport_coe`, `HasFiniteMulSupport.fun_zpow`, `Ideal.finite_mulSupport`, `HasFiniteMulSupport.inf`, `HasFiniteMulSupport.snd`, `HasFiniteMulSupport.prodMk`, `hasFiniteMulSupport_fun_one`, `HasFiniteMulSupport.comp_of_injective`, `Ideal.hasFiniteMulSupport`, `Height.AdmissibleAbsValues.hasFiniteMulSupport`, `HasFiniteMulSupport.fun_inv`, `HasFiniteMulSupport.fun_mul`, `HasFiniteMulSupport.min`, `HasFiniteMulSupport.inf'`, `finprod_def`, `HasFiniteMulSupport.pow`, `Ideal.hasFiniteMulSupport_inv`, `HasFiniteMulSupport.iInf`, `Ideal.finite_mulSupport_inv`
`HasFiniteSupport` 📖	MathDef	51 math math: `HasFiniteSupport.fun_sub`, `DirectSum.finite_support`, `HasFiniteSupport.iSup`, `DirectSum.hasFiniteSupport`, `Summable.finite_support_of_discreteTopology`, `hasFiniteSupport_of_finsum_ne_zero`, `finsum_def'`, `HasFiniteSupport.max`, `HasFiniteSupport.sup`, `HasFiniteSupport.fun_zsmul`, `Finsupp.finite_support`, `HasFiniteSupport.add`, `HasFiniteSupport.fun_add`, `HasFiniteSupport.of_comp`, `Multiset.hasFiniteSupport_fun_nsmul_count`, `HasFiniteSupport.comp`, `finite_support_of_finsum_ne_zero`, `HahnSeries.SummableFamily.smul_support_finite`, `HasFiniteSupport.inf`, `HasFiniteSupport.fst`, `HasFiniteSupport.fun_comp_of_injective`, `HasFiniteSupport.sub`, `HahnSeries.SummableFamily.hasFiniteSupport_smul`, `HasFiniteSupport.inf'`, `finsum_def`, `HasFiniteSupport.neg`, `hasFiniteSupport_zero`, `support_along_fiber_finite_of_finite`, `MvPolynomial.weightedHomogeneousComponent_finsupp`, `HasFiniteSupport.sumMk`, `HasFiniteSupport.iInf`, `HasFiniteSupport.pi`, `Summable.hasFiniteSupport_of_discreteTopology`, `HasFiniteSupport.zsmul`, `HasFiniteSupport.min`, `HasFiniteSupport.sup'`, `HasFiniteSupport.sum`, `Finsupp.hasFiniteSupport`, `PowerSeries.coeff_subst_finite`, `HasFiniteSupport.fun_nsmul`, `HasFiniteSupport.fun_comp`, `hasFiniteSupport_of_finsum_eq_one`, `HasFiniteSupport.fun_neg`, `MvPowerSeries.coeff_subst_finite`, `HasFiniteSupport.snd`, `PowerSeries.coeff_subst_finite'`, `HasFiniteSupport.comp_of_injective`, `finite_support_of_finsum_eq_one`, `HasFiniteSupport.nsmul`, `HahnSeries.SummableFamily.finite_co_support`, `hasFiniteSupport_fun_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasFiniteMulSupport_one` 📖	mathematical	—	`HasFiniteMulSupport`	—	`mulSupport_fun_one`
`hasFiniteSupport_zero` 📖	mathematical	—	`HasFiniteSupport`	—	`support_fun_zero` `Set.finite_empty`

---

← Back to Index