Main results
The main results that the formalization.yaml of FormalFrontier/iwasawa-modules lists under status.main_results at commit e71db96b, 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 |
|---|---|---|---|
Module.isPseudoNull_iff_localizedModule_subsingleton |
theorem | IwasawaModules/PseudoIsomorphism/Basic.lean, line 34 | Sorry count 0. Axioms: propext, Classical.choice, Quot.sound. |
LinearMap.isPseudoIsomorphism_iff_localizedModule_map_bijective |
theorem | IwasawaModules/PseudoIsomorphism/LinearMap.lean, line 67 | Sorry count 0. Axioms: propext, Classical.choice, Quot.sound. |
CompletedGroupAlgebra.proj_ofMonoidAlgebra |
theorem | IwasawaModules/CompletedGroupAlgebra/Basic.lean, line 103 | Sorry count 0. Axioms: propext, Classical.choice, Quot.sound. |
CompletedGroupAlgebra.continuous_iff_proj |
theorem | IwasawaModules/CompletedGroupAlgebra/Topology.lean, line 224 | Sorry count 0. Axioms: propext, Classical.choice, Quot.sound. |
Quoted from the main results in formalization.yaml of FormalFrontier/iwasawa-modules at commit e71db96b, Apache-2.0.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.