All.lean
Nyll.AlgebraicCurves.Models.Gluing.All
0 declarations indexed from sourceView source ↗
Imports11
- Nyll.AlgebraicCurves.Models.Gluing.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart
- Nyll.AlgebraicCurves.Models.Gluing.Scheme_Opens_isAffineOpen_and_finite_aeval_of_twoChart_right
- Nyll.AlgebraicCurves.Models.Gluing.SmoothProperCurve_exists_twoChartPoleDatum_of_section_invModule
- Nyll.AlgebraicCurves.Models.Gluing.SmoothProperCurve_exists_twoChartPoleDatum_transcendental_le_isUnit_of_twoAffineOpenCover
- Nyll.AlgebraicCurves.Models.Gluing.SmoothProperCurve_exists_twoChart_of_section_invModule
- Nyll.AlgebraicCurves.Models.Gluing.SmoothProperCurve_finrank_levelSet_field_of_twoChartPoleDatum
- Nyll.AlgebraicCurves.Models.Gluing.SmoothProperCurve_flat_aeval_of_twoChartPoleDatum
- Nyll.AlgebraicCurves.Models.Gluing.SmoothProperCurve_injective_aeval_tensor_of_twoChartPoleDatum
- Nyll.AlgebraicCurves.Models.Gluing.SmoothProperCurve_levelSet_free_of_twoChartPoleDatum
- Nyll.AlgebraicCurves.Models.Gluing.SmoothProperCurve_nontrivial_tensor_sections_of_twoChartPoleDatum
- Nyll.AlgebraicCurves.Models.Gluing.SmoothProperCurve_transcendental_app_of_twoChart_of_section_mem
Imported by1
This module has no indexed declarations. Its imports and full source are available here.