Main results
The main results that the formalization.yaml of FormalFrontier/integral-closure lists under status.main_results at commit 8f0b15a5, each that the scan finds declared in the file the yaml gives, with its line. They are listed here, not made articles: in several Formal Frontier libraries this list is close to the whole API. The notes are the yaml's.
| Declaration | Kind | Where | Note |
|---|---|---|---|
HenselianLocalRing.isLocalRing_of_isIntegral |
theorem | IntegralClosure/Henselian.lean, line 141 | Sorry count 0. |
RingHom.isLocalRing_of_henselian_of_isIntegral |
theorem | IntegralClosure/Henselian.lean, line 237 | Sorry count 0. |
PrimeSpectrum.comap_isInducing_of_forall_pow_mem_range |
theorem | IntegralClosure/Spectrum/Topology.lean, line 70 | Sorry count 0. |
PrimeSpectrum.isEmbedding_comap_of_forall_pow_mem_range |
theorem | IntegralClosure/Spectrum/Topology.lean, line 92 | Sorry count 0. |
PrimeSpectrum.comap_injective_of_forall_pow_mem_range |
theorem | IntegralClosure/Spectrum.lean, line 51 | Sorry count 0. |
IsIntegrallyClosed.of_linearRetract |
theorem | IntegralClosure/LinearRetract.lean, line 43 | Sorry count 0. Axioms: propext, Classical.choice, Quot.sound. |
Algebra.TensorProduct.rightLinearMap |
def | IntegralClosure/TensorProduct.lean, line 65 | Axioms: propext, Quot.sound. |
Algebra.TensorProduct.rightLinearMap_includeLeft |
theorem | IntegralClosure/TensorProduct.lean, line 74 | Sorry count 0. Axioms: propext, Quot.sound. |
Algebra.TensorProduct.isDomain_left |
theorem | IntegralClosure/TensorProduct.lean, line 81 | Sorry count 0. Axioms: propext, Classical.choice, Quot.sound. |
Algebra.TensorProduct.isIntegrallyClosed_left |
theorem | IntegralClosure/TensorProduct.lean, line 91 | Sorry count 0. Axioms: propext, Classical.choice, Quot.sound. |
Quoted from the main results in formalization.yaml of FormalFrontier/integral-closure at commit 8f0b15a5, Apache-2.0.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.