Lemmas

📁 Source: FLT/Patching/Utils/Lemmas.lean

Statistics

Metric	Count
Definitions idealQuotientEquiv, piMap, liftQuotientₗ, pi', leAddSubgroup, instAlgebraForall_fLT	6
Theorems idealQuotientEquiv_apply_coe, idealQuotientEquiv_symm_apply, maximalIdeal_pow_card_smul_top_le, compactSpace, pi_iff, piMap_apply, liftQuotientₗ_bijective, liftQuotientₗ_surjective, comap_smul_of_le_range, comap_smul_of_surjective, mem_pi', leAddSubgroup_subset, mem_leAddSubgroup, mem_leAddSubgroup', mem_span_singleton, span_le', span_neg, span_singleton_zero, exists_eq_sup, exists_eq_inf, disjoint_nonZeroDivisors_of_mem_minimalPrimes, exists_addSubgroup_isOpen_and_subset, exists_ideal_isOpen_and_subset, exists_subgroup_isOpen_and_subset, exists_twoSidedIdeal_isOpen_and_subset, forall_prod_iff, instCompactSpaceQuotientIdeal_fLT, instTotallyDisconnectedSpaceOfDiscreteTopology_fLT, pi'_jacobson	29
Total	35

Ideal

Definitions

Name	Category	Theorems
idealQuotientEquiv 📖	CompOp	2 math math: idealQuotientEquiv_symm_apply, idealQuotientEquiv_apply_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
idealQuotientEquiv_apply_coe 📖	mathematical	—	idealQuotientEquiv	—	—
idealQuotientEquiv_symm_apply 📖	mathematical	—	idealQuotientEquiv	—	—

IsLocalRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
maximalIdeal_pow_card_smul_top_le 📖	—	—	—	—	WellFoundedLT.exists_eq_inf

IsModuleTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compactSpace 📖	—	—	—	—	—

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pi_iff 📖	—	—	—	—	—

LinearMap

Definitions

Name	Category	Theorems
piMap 📖	CompOp	2 math math: PatchingModule.mapEquiv_apply, piMap_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
piMap_apply 📖	mathematical	—	piMap	—	—

Pi

Definitions

Name	Category	Theorems
liftQuotientₗ 📖	CompOp	2 math math: liftQuotientₗ_bijective, liftQuotientₗ_surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
liftQuotientₗ_bijective 📖	mathematical	—	liftQuotientₗ	—	Submodule.comap_smul_of_surjective liftQuotientₗ_surjective
liftQuotientₗ_surjective 📖	mathematical	—	liftQuotientₗ	—	—

Submodule

Definitions

Name	Category	Theorems
pi' 📖	CompOp	3 math math: pi'_jacobson, eventuallyProd_eq_sup, mem_pi'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_smul_of_le_range 📖	—	—	—	—	—
comap_smul_of_surjective 📖	—	—	—	—	comap_smul_of_le_range
mem_pi' 📖	mathematical	—	pi'	—	—

TwoSidedIdeal

Definitions

Name	Category	Theorems
leAddSubgroup 📖	CompOp	3 math math: mem_leAddSubgroup', mem_leAddSubgroup, leAddSubgroup_subset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
leAddSubgroup_subset 📖	mathematical	—	leAddSubgroup	—	mem_span_singleton
mem_leAddSubgroup 📖	mathematical	—	leAddSubgroup	—	mem_span_singleton
mem_leAddSubgroup' 📖	mathematical	—	leAddSubgroup	—	—
mem_span_singleton 📖	—	—	—	—	—
span_le' 📖	—	—	—	—	—
span_neg 📖	—	—	—	—	span_le'
span_singleton_zero 📖	—	—	—	—	span_le'

WellFoundedGT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_eq_sup 📖	—	—	—	—	—

WellFoundedLT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_eq_inf 📖	—	—	—	—	WellFoundedGT.exists_eq_sup

(root)

Definitions

Name	Category	Theorems
instAlgebraForall_fLT 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
disjoint_nonZeroDivisors_of_mem_minimalPrimes 📖	—	—	—	—	—
exists_addSubgroup_isOpen_and_subset 📖	—	—	—	—	—
exists_ideal_isOpen_and_subset 📖	—	—	—	—	exists_twoSidedIdeal_isOpen_and_subset
exists_subgroup_isOpen_and_subset 📖	—	—	—	—	—
exists_twoSidedIdeal_isOpen_and_subset 📖	—	—	—	—	exists_addSubgroup_isOpen_and_subset TwoSidedIdeal.mem_leAddSubgroup TwoSidedIdeal.leAddSubgroup_subset
forall_prod_iff 📖	—	—	—	—	—
instCompactSpaceQuotientIdeal_fLT 📖	—	—	—	—	—
instTotallyDisconnectedSpaceOfDiscreteTopology_fLT 📖	—	—	—	—	—
pi'_jacobson 📖	mathematical	—	Submodule.pi'	—	forall_prod_iff

---

← Back to Index