All.lean
Nyll.AlgebraicCurves.Hilbert.All
0 declarations indexed from sourceView source ↗
Imports20
- Nyll.AlgebraicCurves.Hilbert.Functor.All
- Nyll.AlgebraicCurves.Hilbert.Point_I_eq_span_of_forall_finrank_piece_succ_le
- Nyll.AlgebraicCurves.Hilbert.Point_flat_comp_of_ideal_basicOpen_eq_span
- Nyll.AlgebraicCurves.Hilbert.exists_cover_forall_finrank_piece_eq_of_isClosedImmersion_of_flat_of_isNoetherianRing
- Nyll.AlgebraicCurves.Hilbert.exists_cover_forall_finrank_piece_eq_of_isClosedImmersion_of_flat_of_locallyOfFinitePresentation
- Nyll.AlgebraicCurves.Hilbert.exists_forall_finrank_piece_eq_eval_of_isClosedImmersion_of_forall_mem_iff_of_eventually_eq
- Nyll.AlgebraicCurves.Hilbert.exists_forall_geomFibreH0Finrank_tensorPow_eq_hilbertFunctionOf_of_point
- Nyll.AlgebraicCurves.Hilbert.exists_ideal_forall_mem_iff_app_awayToSection_eq_zero_and_polynomial
- Nyll.AlgebraicCurves.Hilbert.exists_ideal_forall_projective_piece_succ_iff
- Nyll.AlgebraicCurves.Hilbert.exists_isClosedImmersion_locallyOfFinitePresentation_forall_factors_iff_forall_mem_of_isHomogeneous_of_le_of_fg
- Nyll.AlgebraicCurves.Hilbert.exists_linearEquiv_baseChange_piece_map
- Nyll.AlgebraicCurves.Hilbert.exists_point_I_eq_map
- Nyll.AlgebraicCurves.Hilbert.exists_point_I_eq_span_of_forall_surjective_of_forall_projective
- Nyll.AlgebraicCurves.Hilbert.exists_point_forall_mem_iff_of_isClosedImmersion_of_forall_geomFibreH0Finrank_eq_eval
- Nyll.AlgebraicCurves.Hilbert.exists_point_hilbertFunctionOf_forall_mem_iff_of_forall_finrank_piece_eq
- Nyll.AlgebraicCurves.Hilbert.exists_uniform_cover_forall_geomFibre_ideal_eq_point_of_isClosedImmersion_of_flat_of_locallyOfFinitePresentation
- Nyll.AlgebraicCurves.Hilbert.free_piece_of_isLocalRing_of_forall_relation_mem_span
- Nyll.AlgebraicCurves.Hilbert.map_mem_iff_tmul_mkQ_piece_eq_zero
- Nyll.AlgebraicCurves.Hilbert.mem_of_forall_exists_X_pow_mul_mem_of_forall_mem_iff_app_awayToSection_eq_zero
- Nyll.AlgebraicCurves.Hilbert.SymmetricPowerData
Imported by1
This module has no indexed declarations. Its imports and full source are available here.