Section5

📁 Source: Hochster/Section5.lean

Statistics

Metric	Count
Definitions NonVanishingConstSetsFromInter, iSupExtForVIsSimple, indExtForVIsSimple, indExtForVSuccIsSimple, isSimple, F, field, h, mapRingHomToPiFractionRingIsSimple	9
Theorems map_apply_eq_map_apply_of_mem_of_mem_of_apply_eq, map_apply_ne_zero_of_forall_mem_of_forall_ne_zero_of_apply_eq, sUnion_eq, exists_mem_span_and_eq_biInter_of_isSimple, exists_mem_span_and_forall_apply_eq_zero_iff_and_of_isSimple, exists_mem_span_and_forall_apply_eq_zero_iff_forall_of_isSimple, exists_mem_span_and_forall_map_apply_eq_zero_iff_and_of_isSimple, finite_nonVanishingConstSetsFromInter_of_isSimple, iSupExtForV_springLike_spring_isAffine_of_isSimple, indExtForVIsSimple_f, indExtForVIsSimple_h, indExtForVIsSimple_h', forall_finite, forall_injective, springLike_spring_isAffine_of_isSimple_of_forall_imp, map_apply_eq_map_apply_of_pi_of_eq_of_eq, map_apply_eq_zero_of_pi_of_eq_of_eq_of_mem_span_of_eq	17
Total	26

NonVanishingConstSetsFromInter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_apply_eq_map_apply_of_mem_of_mem_of_apply_eq 📖	—	NonVanishingConstSetsFromInter	—	—	Subring.map_apply_eq_map_apply_of_pi_of_eq_of_eq
map_apply_ne_zero_of_forall_mem_of_forall_ne_zero_of_apply_eq 📖	—	—	—	—	sUnion_eq map_apply_eq_map_apply_of_mem_of_mem_of_apply_eq
sUnion_eq 📖	mathematical	—	NonVanishingConstSetsFromInter	—	—

SpringLike'

Definitions

Name	Category	Theorems
isSimple 📖	CompData	—
mapRingHomToPiFractionRingIsSimple 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_mem_span_and_eq_biInter_of_isSimple 📖	—	SpringLike'	—	—	exists_mem_span_and_forall_apply_eq_zero_iff_forall_of_isSimple
exists_mem_span_and_forall_apply_eq_zero_iff_and_of_isSimple 📖	—	SpringLike'	—	—	exists_mem_span_and_forall_map_apply_eq_zero_iff_and_of_isSimple isSimple.forall_injective
exists_mem_span_and_forall_apply_eq_zero_iff_forall_of_isSimple 📖	—	SpringLike'	—	—	exists_mem_span_and_forall_apply_eq_zero_iff_and_of_isSimple
exists_mem_span_and_forall_map_apply_eq_zero_iff_and_of_isSimple 📖	mathematical	SpringLike'	isSimple.F isSimple.field isSimple.h	—	SpringLike.mem_matchingIdeal_iff_eq_zero finite_nonVanishingConstSetsFromInter_of_isSimple SpringLike.matchingIdeal_isPrime NonVanishingConstSetsFromInter.map_apply_ne_zero_of_forall_mem_of_forall_ne_zero_of_apply_eq isSimple.forall_injective Subring.map_apply_eq_zero_of_pi_of_eq_of_eq_of_mem_span_of_eq
finite_nonVanishingConstSetsFromInter_of_isSimple 📖	mathematical	SpringLike'	NonVanishingConstSetsFromInter isSimple.F isSimple.field isSimple.h	—	isSimple.forall_finite
springLike_spring_isAffine_of_isSimple_of_forall_imp 📖	mathematical	SpringLike'	SpringCat.isAffine SpringLike.spring springLike	—	springLike_spring_isAffine_iff_forall_mem_radical_of_subset exists_mem_span_and_eq_biInter_of_isSimple

SpringLike'.isIndex

Definitions

Name	Category	Theorems
iSupExtForVIsSimple 📖	CompOp	—
indExtForVIsSimple 📖	CompOp	3 math math: indExtForVIsSimple_h, indExtForVIsSimple_h', indExtForVIsSimple_f
indExtForVSuccIsSimple 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iSupExtForV_springLike_spring_isAffine_of_isSimple 📖	mathematical	SpringLike' SpringLike'.isIndex	SpringCat.isAffine SpringLike.spring ISupExtForV SpringLike'.springLike iSupExtForV	—	SpringLike'.springLike_spring_isAffine_of_isSimple_of_forall_imp mem_radical_span_singleton_of_forall_imp
indExtForVIsSimple_f 📖	mathematical	SpringLike' SpringLike'.isIndex	SpringLike'.isSimple.F IndExtForV indExtForV indExtForVIsSimple	—	indExtForV
indExtForVIsSimple_h 📖	mathematical	SpringLike' SpringLike'.isIndex	SpringLike'.isSimple.h IndExtForV indExtForV indExtForVIsSimple	—	indExtForV
indExtForVIsSimple_h' 📖	mathematical	SpringLike' SpringLike'.isIndex	SpringLike'.isSimple.F IndExtForV indExtForV indExtForVIsSimple SpringLike'.isSimple.field SpringLike'.isSimple.h indExtForVIsSimple_f	—	indExtForV indExtForVIsSimple_f

SpringLike'.isSimple

Definitions

Name	Category	Theorems
F 📖	CompOp	6 math math: SpringLike'.finite_nonVanishingConstSetsFromInter_of_isSimple, forall_injective, SpringLike'.exists_mem_span_and_forall_map_apply_eq_zero_iff_and_of_isSimple, SpringLike'.isIndex.indExtForVIsSimple_h', forall_finite, SpringLike'.isIndex.indExtForVIsSimple_f
field 📖	CompOp	5 math math: SpringLike'.finite_nonVanishingConstSetsFromInter_of_isSimple, forall_injective, SpringLike'.exists_mem_span_and_forall_map_apply_eq_zero_iff_and_of_isSimple, SpringLike'.isIndex.indExtForVIsSimple_h', forall_finite
h 📖	CompOp	6 math math: SpringLike'.finite_nonVanishingConstSetsFromInter_of_isSimple, SpringLike'.isIndex.indExtForVIsSimple_h, forall_injective, SpringLike'.exists_mem_span_and_forall_map_apply_eq_zero_iff_and_of_isSimple, SpringLike'.isIndex.indExtForVIsSimple_h', forall_finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forall_finite 📖	mathematical	SpringLike'	F field h	—	—
forall_injective 📖	mathematical	SpringLike'	F field h	—	—

Subring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_apply_eq_map_apply_of_pi_of_eq_of_eq 📖	—	—	—	—	—
map_apply_eq_zero_of_pi_of_eq_of_eq_of_mem_span_of_eq 📖	—	—	—	—	—

(root)

Definitions

Name	Category	Theorems
NonVanishingConstSetsFromInter 📖	CompOp	2 math math: SpringLike'.finite_nonVanishingConstSetsFromInter_of_isSimple, NonVanishingConstSetsFromInter.sUnion_eq

---

← Back to Index