Section6

Statistics

Metric	Count
Definitions `SWICat`, `E`, `Hom`, `comp`, `f`, `id`, `r`, `T`, `X`, `closureRangeUnionIsSimple`, `evalMapApplyPoly`, `g`, `instCategory`, `preV`, `tX`, `v`, `valuationFun`, `repMvPoly`, `repMvPoly'`, `repMvPoly''`	20
Theorems `support_mul_C_of_ne_zero`, `comp_eq_comp`, `injective`, `isSpectralMap`, `T_apply_eq_zero_iff`, `T_apply_ne_zero_iff`, `T_mul_T_support_eq_inter`, `T_support_eq_g`, `coeff_evalMapApplyPoly`, `eq_generateFrom`, `evalMapApplyPoly_C`, `evalMapApplyPoly_X`, `evalMapApplyPoly_add`, `evalMapApplyPoly_def`, `evalMapApplyPoly_monomial`, `evalMapApplyPoly_monomial_support_eq_biInter`, `evalMapApplyPoly_mul`, `evalMapApplyPoly_ne_zero_iff_valuationFun_apply_evalMapApplyPoly_eq_one`, `evalMapApplyPoly_one`, `evalMapApplyPoly_prod`, `evalMapApplyPoly_sum`, `evalMapApplyPoly_support_eq_biUnion`, `evalMapApplyPoly_support_eq_biUnion_biInter`, `evalMapApplyPoly_zero`, `eval_map_ringHom_apply_eq_eval_map_C_apply'`, `exists_valuationFun_apply_eq_two_pow_of_ne_zero`, `ext`, `ext_iff`, `finite_evalMapApplyPoly_image`, `finite_image_T`, `forall_isCompact`, `forall_isOpen`, `isCompact_evalMapApplyPoly_support`, `isOpen_evalMapApplyPoly_support`, `prod_T_support_eq_biInter`, `prod_le_valuationFun_apply_of_mem_support`, `spectralSpace`, `springLike'`, `springLike'_mapRingHomToPiFractionRing_isIndex`, `support_evalMapApplyPoly`, `support_evalMapApplyPoly_subset`, `v_apply_ringHomToPiFractionRing_apply`, `v_apply_ringHomToPiFractionRing_apply'`, `valuationFun_apply_C`, `valuationFun_apply_X`, `valuationFun_apply_add_eq_apply_of_lt`, `valuationFun_apply_add_le_max`, `valuationFun_apply_eq_iff_exist_of_support_nonempty`, `valuationFun_apply_eq_iff_of_ne_zero`, `valuationFun_apply_eq_iff_of_ne_zero'`, `valuationFun_apply_eq_iff_of_support_nonempty`, `valuationFun_apply_eq_iff_of_support_nonempty'`, `valuationFun_apply_eq_of_forall_prod_eq`, `valuationFun_apply_eq_of_forall_valuationFun_apply_eq`, `valuationFun_apply_eq_zero_iff`, `valuationFun_apply_le_iff_forall_prod_le`, `valuationFun_apply_le_iff_forall_valuationFun_apply_le`, `valuationFun_apply_le_one`, `valuationFun_apply_lt_iff_forall_prod_lt_of_ne_zero`, `valuationFun_apply_lt_iff_forall_prod_lt_of_support_nonempty`, `valuationFun_apply_lt_iff_forall_valuationFun_apply_lt_of_ne_zero`, `valuationFun_apply_lt_iff_forall_valuationFun_apply_lt_of_support_nonempty`, `valuationFun_apply_monomial`, `valuationFun_apply_monomial_mul_monomial`, `valuationFun_apply_mul`, `valuationFun_apply_mul_eq_of_forall_of_forall`, `valuationFun_apply_mul_le_mul`, `valuationFun_apply_of_support_nonempty`, `valuationFun_apply_zero`, `coeff_repMvPoly_mem`, `exists_mvPolynomial_of_le_range_of_mem_closure`, `exists_mvPolynomial_of_le_range_of_subset_range_of_mem_closure`, `exists_mvPolynomial_of_mem_closure`, `exists_mvPolynomial_of_mem_closure'`, `map_repMvPoly''_eval_eq`, `map_repMvPoly'_eval_eq`, `repMvPoly_eval_eq`	77
Total	97

MvPolynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`support_mul_C_of_ne_zero` 📖	—	—	—	—	—

SWICat

Definitions

Name	Category	Theorems
`E` 📖	CompOp	49 math math: `valuationFun_apply_lt_iff_forall_prod_lt_of_ne_zero`, `valuationFun_apply_add_le_max`, `prod_T_support_eq_biInter`, `support_evalMapApplyPoly_subset`, `finite_image_T`, `T_mul_T_support_eq_inter`, `evalMapApplyPoly_one`, `valuationFun_apply_add_eq_apply_of_lt`, `eq_generateFrom`, `valuationFun_apply_eq_zero_iff`, `ext_iff`, `evalMapApplyPoly_mul`, `valuationFun_apply_lt_iff_forall_valuationFun_apply_lt_of_ne_zero`, `valuationFun_apply_eq_iff_of_ne_zero'`, `evalMapApplyPoly_monomial`, `valuationFun_apply_zero`, `evalMapApplyPoly_add`, `evalMapApplyPoly_def`, `evalMapApplyPoly_support_eq_biUnion_biInter`, `Hom.injective`, `v_apply_ringHomToPiFractionRing_apply'`, `valuationFun_apply_monomial_mul_monomial`, `Hom.comp_eq_comp`, `valuationFun_apply_C`, `springLike'`, `isOpen_evalMapApplyPoly_support`, `valuationFun_apply_X`, `valuationFun_apply_le_iff_forall_valuationFun_apply_le`, `finite_evalMapApplyPoly_image`, `evalMapApplyPoly_X`, `T_apply_eq_zero_iff`, `valuationFun_apply_monomial`, `springLike'_mapRingHomToPiFractionRing_isIndex`, `eval_map_ringHom_apply_eq_eval_map_C_apply'`, `T_support_eq_g`, `v_apply_ringHomToPiFractionRing_apply`, `evalMapApplyPoly_C`, `valuationFun_apply_le_iff_forall_prod_le`, `valuationFun_apply_eq_iff_of_ne_zero`, `valuationFun_apply_mul_le_mul`, `evalMapApplyPoly_sum`, `support_evalMapApplyPoly`, `coeff_evalMapApplyPoly`, `valuationFun_apply_mul`, `evalMapApplyPoly_monomial_support_eq_biInter`, `evalMapApplyPoly_prod`, `evalMapApplyPoly_zero`, `evalMapApplyPoly_support_eq_biUnion`, `isCompact_evalMapApplyPoly_support`
`Hom` 📖	CompData	—
`T` 📖	CompOp	10 math math: `prod_T_support_eq_biInter`, `finite_image_T`, `T_mul_T_support_eq_inter`, `evalMapApplyPoly_def`, `springLike'`, `evalMapApplyPoly_X`, `T_apply_eq_zero_iff`, `springLike'_mapRingHomToPiFractionRing_isIndex`, `eval_map_ringHom_apply_eq_eval_map_C_apply'`, `T_support_eq_g`
`X` 📖	CompOp	37 math math: `valuationFun_apply_lt_iff_forall_prod_lt_of_ne_zero`, `prod_T_support_eq_biInter`, `finite_image_T`, `T_mul_T_support_eq_inter`, `T_apply_ne_zero_iff`, `eq_generateFrom`, `ext_iff`, `prod_le_valuationFun_apply_of_mem_support`, `evalMapApplyPoly_ne_zero_iff_valuationFun_apply_evalMapApplyPoly_eq_one`, `forall_isCompact`, `spectralSpace`, `evalMapApplyPoly_monomial`, `evalMapApplyPoly_def`, `evalMapApplyPoly_support_eq_biUnion_biInter`, `valuationFun_apply_of_support_nonempty`, `valuationFun_apply_eq_iff_of_support_nonempty`, `v_apply_ringHomToPiFractionRing_apply'`, `forall_isOpen`, `Hom.comp_eq_comp`, `Hom.isSpectralMap`, `springLike'`, `isOpen_evalMapApplyPoly_support`, `valuationFun_apply_X`, `finite_evalMapApplyPoly_image`, `T_apply_eq_zero_iff`, `valuationFun_apply_monomial`, `springLike'_mapRingHomToPiFractionRing_isIndex`, `eval_map_ringHom_apply_eq_eval_map_C_apply'`, `T_support_eq_g`, `v_apply_ringHomToPiFractionRing_apply`, `valuationFun_apply_le_iff_forall_prod_le`, `valuationFun_apply_eq_iff_of_ne_zero`, `valuationFun_apply_lt_iff_forall_prod_lt_of_support_nonempty`, `coeff_evalMapApplyPoly`, `evalMapApplyPoly_monomial_support_eq_biInter`, `evalMapApplyPoly_support_eq_biUnion`, `isCompact_evalMapApplyPoly_support`
`closureRangeUnionIsSimple` 📖	CompOp	—
`evalMapApplyPoly` 📖	CompOp	20 math math: `support_evalMapApplyPoly_subset`, `evalMapApplyPoly_one`, `evalMapApplyPoly_ne_zero_iff_valuationFun_apply_evalMapApplyPoly_eq_one`, `evalMapApplyPoly_mul`, `evalMapApplyPoly_monomial`, `evalMapApplyPoly_add`, `evalMapApplyPoly_def`, `evalMapApplyPoly_support_eq_biUnion_biInter`, `isOpen_evalMapApplyPoly_support`, `finite_evalMapApplyPoly_image`, `evalMapApplyPoly_X`, `evalMapApplyPoly_C`, `evalMapApplyPoly_sum`, `support_evalMapApplyPoly`, `coeff_evalMapApplyPoly`, `evalMapApplyPoly_monomial_support_eq_biInter`, `evalMapApplyPoly_prod`, `evalMapApplyPoly_zero`, `evalMapApplyPoly_support_eq_biUnion`, `isCompact_evalMapApplyPoly_support`
`g` 📖	CompOp	22 math math: `valuationFun_apply_lt_iff_forall_prod_lt_of_ne_zero`, `prod_T_support_eq_biInter`, `T_apply_ne_zero_iff`, `eq_generateFrom`, `ext_iff`, `prod_le_valuationFun_apply_of_mem_support`, `forall_isCompact`, `evalMapApplyPoly_monomial`, `evalMapApplyPoly_support_eq_biUnion_biInter`, `valuationFun_apply_of_support_nonempty`, `valuationFun_apply_eq_iff_of_support_nonempty`, `forall_isOpen`, `Hom.comp_eq_comp`, `valuationFun_apply_X`, `T_apply_eq_zero_iff`, `valuationFun_apply_monomial`, `T_support_eq_g`, `valuationFun_apply_le_iff_forall_prod_le`, `valuationFun_apply_eq_iff_of_ne_zero`, `valuationFun_apply_lt_iff_forall_prod_lt_of_support_nonempty`, `coeff_evalMapApplyPoly`, `evalMapApplyPoly_monomial_support_eq_biInter`
`instCategory` 📖	CompOp	—
`preV` 📖	CompOp	2 math math: `v_apply_ringHomToPiFractionRing_apply'`, `v_apply_ringHomToPiFractionRing_apply`
`tX` 📖	CompOp	22 math math: `valuationFun_apply_lt_iff_forall_prod_lt_of_ne_zero`, `eq_generateFrom`, `ext_iff`, `prod_le_valuationFun_apply_of_mem_support`, `evalMapApplyPoly_ne_zero_iff_valuationFun_apply_evalMapApplyPoly_eq_one`, `forall_isCompact`, `spectralSpace`, `valuationFun_apply_of_support_nonempty`, `valuationFun_apply_eq_iff_of_support_nonempty`, `v_apply_ringHomToPiFractionRing_apply'`, `forall_isOpen`, `Hom.isSpectralMap`, `springLike'`, `isOpen_evalMapApplyPoly_support`, `valuationFun_apply_X`, `valuationFun_apply_monomial`, `springLike'_mapRingHomToPiFractionRing_isIndex`, `v_apply_ringHomToPiFractionRing_apply`, `valuationFun_apply_le_iff_forall_prod_le`, `valuationFun_apply_eq_iff_of_ne_zero`, `valuationFun_apply_lt_iff_forall_prod_lt_of_support_nonempty`, `isCompact_evalMapApplyPoly_support`
`v` 📖	CompOp	3 math math: `v_apply_ringHomToPiFractionRing_apply'`, `springLike'_mapRingHomToPiFractionRing_isIndex`, `v_apply_ringHomToPiFractionRing_apply`
`valuationFun` 📖	CompOp	26 math math: `valuationFun_apply_lt_iff_forall_prod_lt_of_ne_zero`, `valuationFun_apply_add_le_max`, `valuationFun_apply_lt_iff_forall_valuationFun_apply_lt_of_support_nonempty`, `valuationFun_apply_eq_zero_iff`, `prod_le_valuationFun_apply_of_mem_support`, `evalMapApplyPoly_ne_zero_iff_valuationFun_apply_evalMapApplyPoly_eq_one`, `valuationFun_apply_eq_of_forall_prod_eq`, `valuationFun_apply_lt_iff_forall_valuationFun_apply_lt_of_ne_zero`, `valuationFun_apply_le_one`, `valuationFun_apply_eq_iff_of_ne_zero'`, `valuationFun_apply_zero`, `valuationFun_apply_of_support_nonempty`, `valuationFun_apply_eq_iff_of_support_nonempty`, `valuationFun_apply_monomial_mul_monomial`, `valuationFun_apply_eq_iff_exist_of_support_nonempty`, `valuationFun_apply_C`, `valuationFun_apply_X`, `valuationFun_apply_le_iff_forall_valuationFun_apply_le`, `valuationFun_apply_monomial`, `valuationFun_apply_le_iff_forall_prod_le`, `valuationFun_apply_eq_iff_of_ne_zero`, `valuationFun_apply_mul_le_mul`, `valuationFun_apply_lt_iff_forall_prod_lt_of_support_nonempty`, `valuationFun_apply_eq_iff_of_support_nonempty'`, `exists_valuationFun_apply_eq_two_pow_of_ne_zero`, `valuationFun_apply_mul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`T_apply_eq_zero_iff` 📖	mathematical	—	`T` `E` `X` `g`	—	—
`T_apply_ne_zero_iff` 📖	mathematical	—	`X` `g`	—	—
`T_mul_T_support_eq_inter` 📖	mathematical	—	`X` `E` `T`	—	—
`T_support_eq_g` 📖	mathematical	—	`X` `E` `T` `g`	—	—
`coeff_evalMapApplyPoly` 📖	mathematical	—	`E` `evalMapApplyPoly` `X` `g`	—	`evalMapApplyPoly_add` `evalMapApplyPoly_monomial`
`eq_generateFrom` 📖	mathematical	—	`tX` `X` `E` `g`	—	—
`evalMapApplyPoly_C` 📖	mathematical	—	`evalMapApplyPoly` `E`	—	—
`evalMapApplyPoly_X` 📖	mathematical	—	`evalMapApplyPoly` `E` `T`	—	—
`evalMapApplyPoly_add` 📖	mathematical	—	`evalMapApplyPoly` `E`	—	—
`evalMapApplyPoly_def` 📖	mathematical	—	`evalMapApplyPoly` `E` `X` `T`	—	—
`evalMapApplyPoly_monomial` 📖	mathematical	—	`evalMapApplyPoly` `E` `X` `g`	—	—
`evalMapApplyPoly_monomial_support_eq_biInter` 📖	mathematical	—	`X` `E` `evalMapApplyPoly` `g`	—	`evalMapApplyPoly_monomial`
`evalMapApplyPoly_mul` 📖	mathematical	—	`evalMapApplyPoly` `E`	—	—
`evalMapApplyPoly_ne_zero_iff_valuationFun_apply_evalMapApplyPoly_eq_one` 📖	mathematical	—	`valuationFun` `evalMapApplyPoly` `X` `MemClosurePairs.z` `tX`	—	`evalMapApplyPoly_support_eq_biUnion_biInter` `MemClosurePairs.mem_closure` `forall_isOpen` `support_evalMapApplyPoly` `valuationFun_apply_eq_iff_of_support_nonempty'` `valuationFun_apply_le_one` `valuationFun_apply_monomial` `valuationFun_apply_eq_iff_of_ne_zero'` `support_evalMapApplyPoly_subset`
`evalMapApplyPoly_one` 📖	mathematical	—	`evalMapApplyPoly` `E`	—	—
`evalMapApplyPoly_prod` 📖	mathematical	—	`evalMapApplyPoly` `E`	—	—
`evalMapApplyPoly_sum` 📖	mathematical	—	`evalMapApplyPoly` `E`	—	—
`evalMapApplyPoly_support_eq_biUnion` 📖	mathematical	—	`X` `E` `evalMapApplyPoly`	—	`support_evalMapApplyPoly_subset` `coeff_evalMapApplyPoly` `evalMapApplyPoly_monomial`
`evalMapApplyPoly_support_eq_biUnion_biInter` 📖	mathematical	—	`X` `E` `evalMapApplyPoly` `g`	—	`evalMapApplyPoly_support_eq_biUnion` `evalMapApplyPoly_monomial_support_eq_biInter`
`evalMapApplyPoly_zero` 📖	mathematical	—	`evalMapApplyPoly` `E`	—	—
`eval_map_ringHom_apply_eq_eval_map_C_apply'` 📖	mathematical	—	`E` `X` `T`	—	—
`exists_valuationFun_apply_eq_two_pow_of_ne_zero` 📖	mathematical	—	`valuationFun`	—	`valuationFun_apply_eq_iff_of_support_nonempty`
`ext` 📖	—	`X` `tX` `E` `g`	—	—	—
`ext_iff` 📖	mathematical	—	`X` `tX` `E` `g`	—	`ext`
`finite_evalMapApplyPoly_image` 📖	mathematical	—	`E` `X` `evalMapApplyPoly`	—	`evalMapApplyPoly_C` `evalMapApplyPoly_add` `evalMapApplyPoly_mul` `evalMapApplyPoly_X` `finite_image_T`
`finite_image_T` 📖	mathematical	—	`E` `X` `T`	—	—
`forall_isCompact` 📖	mathematical	—	`X` `tX` `g`	—	—
`forall_isOpen` 📖	mathematical	—	`X` `tX` `g`	—	—
`isCompact_evalMapApplyPoly_support` 📖	mathematical	—	`X` `tX` `E` `evalMapApplyPoly`	—	`Finset.biInter_mem_of_finiteInter` `finiteInter_isOpen_and_isCompact` `spectralSpace` `forall_isOpen` `forall_isCompact` `evalMapApplyPoly_support_eq_biUnion_biInter`
`isOpen_evalMapApplyPoly_support` 📖	mathematical	—	`X` `tX` `E` `evalMapApplyPoly`	—	`forall_isOpen` `evalMapApplyPoly_support_eq_biUnion_biInter`
`prod_T_support_eq_biInter` 📖	mathematical	—	`X` `E` `T` `g`	—	`T_apply_ne_zero_iff`
`prod_le_valuationFun_apply_of_mem_support` 📖	mathematical	`E`	`X` `g` `MemClosurePairs.z` `tX` `valuationFun`	—	—
`spectralSpace` 📖	mathematical	—	`X` `tX`	—	—
`springLike'` 📖	mathematical	—	`SpringLike'` `X` `tX` `E` `T`	—	`spectralSpace` `Subring.exists_mvPolynomial_of_le_range_of_subset_range_of_mem_closure` `isOpen_evalMapApplyPoly_support` `isCompact_evalMapApplyPoly_support` `eq_generateFrom` `prod_T_support_eq_biInter`
`springLike'_mapRingHomToPiFractionRing_isIndex` 📖	mathematical	—	`SpringLike'.isIndex` `X` `tX` `E` `Pi.ringHomToPiFractionRing` `T` `SpringLike'.mapRingHomToPiFractionRing` `springLike'` `v`	—	`SpringLike'.mapRingHomToPiFractionRing` `springLike'` `valuationFun_apply_zero` `valuationFun_apply_mul` `valuationFun_apply_add_le_max` `exists_valuationFun_apply_eq_two_pow_of_ne_zero` `valuationFun_apply_le_one` `v_apply_ringHomToPiFractionRing_apply` `Subring.exists_mvPolynomial_of_le_range_of_subset_range_of_mem_closure` `evalMapApplyPoly_ne_zero_iff_valuationFun_apply_evalMapApplyPoly_eq_one` `valuationFun_apply_eq_iff_of_support_nonempty` `support_evalMapApplyPoly_subset`
`support_evalMapApplyPoly` 📖	mathematical	—	`E` `evalMapApplyPoly`	—	`coeff_evalMapApplyPoly`
`support_evalMapApplyPoly_subset` 📖	mathematical	—	`E` `evalMapApplyPoly`	—	`support_evalMapApplyPoly`
`v_apply_ringHomToPiFractionRing_apply` 📖	mathematical	—	`E` `v` `X` `Pi.ringHomToPiFractionRing` `MemClosurePairs.z` `tX` `preV`	—	—
`v_apply_ringHomToPiFractionRing_apply'` 📖	mathematical	—	`E` `v` `X` `Pi.ringHomToPiFractionRing` `MemClosurePairs.z` `tX` `preV`	—	—
`valuationFun_apply_C` 📖	mathematical	—	`valuationFun` `E`	—	`valuationFun_apply_zero` `valuationFun_apply_of_support_nonempty`
`valuationFun_apply_X` 📖	mathematical	—	`valuationFun` `E` `X` `g` `MemClosurePairs.z` `tX`	—	`valuationFun_apply_of_support_nonempty`
`valuationFun_apply_add_eq_apply_of_lt` 📖	mathematical	`valuationFun`	`E`	—	`valuationFun_apply_zero` `valuationFun_apply_eq_iff_of_support_nonempty` `prod_le_valuationFun_apply_of_mem_support`
`valuationFun_apply_add_le_max` 📖	mathematical	—	`valuationFun` `E`	—	`valuationFun_apply_le_iff_forall_prod_le` `prod_le_valuationFun_apply_of_mem_support`
`valuationFun_apply_eq_iff_exist_of_support_nonempty` 📖	mathematical	`E`	`valuationFun`	—	`valuationFun_apply_lt_iff_forall_valuationFun_apply_lt_of_ne_zero` `valuationFun_apply_eq_zero_iff` `valuationFun_apply_le_iff_forall_valuationFun_apply_le` `valuationFun_apply_eq_iff_of_support_nonempty` `valuationFun_apply_monomial` `valuationFun_apply_add_eq_apply_of_lt` `valuationFun_apply_eq_of_forall_valuationFun_apply_eq`
`valuationFun_apply_eq_iff_of_ne_zero` 📖	mathematical	—	`valuationFun` `E` `X` `g` `MemClosurePairs.z` `tX`	—	`valuationFun_apply_eq_iff_of_support_nonempty` `valuationFun_apply_zero`
`valuationFun_apply_eq_iff_of_ne_zero'` 📖	mathematical	—	`valuationFun` `E`	—	`valuationFun_apply_monomial` `valuationFun_apply_eq_iff_of_ne_zero`
`valuationFun_apply_eq_iff_of_support_nonempty` 📖	mathematical	`E`	`valuationFun` `X` `g` `MemClosurePairs.z` `tX`	—	`prod_le_valuationFun_apply_of_mem_support` `valuationFun_apply_of_support_nonempty`
`valuationFun_apply_eq_iff_of_support_nonempty'` 📖	mathematical	`E`	`valuationFun`	—	`valuationFun_apply_monomial` `valuationFun_apply_eq_iff_of_support_nonempty`
`valuationFun_apply_eq_of_forall_prod_eq` 📖	mathematical	`E` `X` `g` `MemClosurePairs.z` `tX`	`valuationFun`	—	`valuationFun_apply_eq_iff_of_support_nonempty`
`valuationFun_apply_eq_of_forall_valuationFun_apply_eq` 📖	—	`E` `valuationFun`	—	—	`valuationFun_apply_eq_of_forall_prod_eq` `valuationFun_apply_monomial`
`valuationFun_apply_eq_zero_iff` 📖	mathematical	—	`valuationFun` `E`	—	`valuationFun_apply_eq_iff_of_support_nonempty` `valuationFun_apply_zero`
`valuationFun_apply_le_iff_forall_prod_le` 📖	mathematical	—	`valuationFun` `E` `X` `g` `MemClosurePairs.z` `tX`	—	—
`valuationFun_apply_le_iff_forall_valuationFun_apply_le` 📖	mathematical	—	`valuationFun` `E`	—	`valuationFun_apply_monomial` `valuationFun_apply_le_iff_forall_prod_le`
`valuationFun_apply_le_one` 📖	mathematical	—	`valuationFun`	—	—
`valuationFun_apply_lt_iff_forall_prod_lt_of_ne_zero` 📖	mathematical	—	`valuationFun` `E` `X` `g` `MemClosurePairs.z` `tX`	—	—
`valuationFun_apply_lt_iff_forall_prod_lt_of_support_nonempty` 📖	mathematical	`E`	`valuationFun` `X` `g` `MemClosurePairs.z` `tX`	—	`valuationFun_apply_of_support_nonempty`
`valuationFun_apply_lt_iff_forall_valuationFun_apply_lt_of_ne_zero` 📖	mathematical	—	`valuationFun` `E`	—	`valuationFun_apply_monomial` `valuationFun_apply_lt_iff_forall_prod_lt_of_ne_zero`
`valuationFun_apply_lt_iff_forall_valuationFun_apply_lt_of_support_nonempty` 📖	mathematical	`E`	`valuationFun`	—	`valuationFun_apply_monomial` `valuationFun_apply_lt_iff_forall_prod_lt_of_support_nonempty`
`valuationFun_apply_monomial` 📖	mathematical	—	`valuationFun` `E` `X` `g` `MemClosurePairs.z` `tX`	—	`valuationFun_apply_zero`
`valuationFun_apply_monomial_mul_monomial` 📖	mathematical	—	`valuationFun` `E`	—	`valuationFun_apply_monomial`
`valuationFun_apply_mul` 📖	mathematical	—	`valuationFun` `E`	—	`valuationFun_apply_eq_iff_exist_of_support_nonempty` `valuationFun_apply_mul_eq_of_forall_of_forall` `valuationFun_apply_eq_zero_iff` `valuationFun_apply_add_eq_apply_of_lt` `valuationFun_apply_add_le_max` `valuationFun_apply_mul_le_mul` `valuationFun_apply_eq_of_forall_valuationFun_apply_eq` `valuationFun_apply_zero`
`valuationFun_apply_mul_eq_of_forall_of_forall` 📖	—	`E` `valuationFun`	—	—	`valuationFun_apply_eq_of_forall_valuationFun_apply_eq` `valuationFun_apply_monomial_mul_monomial`
`valuationFun_apply_mul_le_mul` 📖	mathematical	—	`valuationFun` `E`	—	`valuationFun_apply_le_iff_forall_prod_le` `valuationFun_apply_le_iff_forall_valuationFun_apply_le` `valuationFun_apply_monomial_mul_monomial` `valuationFun_apply_monomial`
`valuationFun_apply_of_support_nonempty` 📖	mathematical	`E`	`valuationFun` `X` `g` `MemClosurePairs.z` `tX`	—	—
`valuationFun_apply_zero` 📖	mathematical	—	`valuationFun` `E`	—	—

SWICat.Hom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	—
`f` 📖	CompOp	2 math math: `comp_eq_comp`, `isSpectralMap`
`id` 📖	CompOp	—
`r` 📖	CompOp	2 math math: `injective`, `comp_eq_comp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_eq_comp` 📖	mathematical	—	`SWICat.E` `SWICat.X` `SWICat.g` `r` `f`	—	—
`injective` 📖	mathematical	—	`SWICat.E` `r`	—	—
`isSpectralMap` 📖	mathematical	—	`SWICat.X` `SWICat.tX` `f`	—	—

Subring

Definitions

Name	Category	Theorems
`repMvPoly` 📖	CompOp	2 math math: `repMvPoly_eval_eq`, `coeff_repMvPoly_mem`
`repMvPoly'` 📖	CompOp	1 math math: `map_repMvPoly'_eval_eq`
`repMvPoly''` 📖	CompOp	1 math math: `map_repMvPoly''_eval_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_repMvPoly_mem` 📖	mathematical	—	`repMvPoly`	—	`exists_mvPolynomial_of_mem_closure`
`exists_mvPolynomial_of_le_range_of_mem_closure` 📖	—	—	—	—	—
`exists_mvPolynomial_of_le_range_of_subset_range_of_mem_closure` 📖	—	—	—	—	—
`exists_mvPolynomial_of_mem_closure` 📖	—	—	—	—	`exists_mvPolynomial_of_mem_closure'`
`exists_mvPolynomial_of_mem_closure'` 📖	—	—	—	—	—
`map_repMvPoly''_eval_eq` 📖	mathematical	—	`repMvPoly''`	—	`exists_mvPolynomial_of_le_range_of_subset_range_of_mem_closure`
`map_repMvPoly'_eval_eq` 📖	mathematical	—	`repMvPoly'`	—	`exists_mvPolynomial_of_le_range_of_mem_closure`
`repMvPoly_eval_eq` 📖	mathematical	—	`repMvPoly`	—	`exists_mvPolynomial_of_mem_closure`

(root)

Definitions

Name	Category	Theorems
`SWICat` 📖	CompData	—

---

← Back to Index