All.lean
Nyll.AlgebraicCurves.Foundations.Algebra.All
0 declarations indexed from sourceView source ↗
Imports135
- Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_DescentCofaces
- Nyll.AlgebraicCurves.Foundations.Algebra.Mathlib_Algebra_IsDirectLimit
- Nyll.AlgebraicCurves.Foundations.Algebra.Nat_MacaulayPow
- Nyll.AlgebraicCurves.Foundations.Algebra.PresheafOfModules_ExteriorPower
- Nyll.SchemeTheory.Modules.PresheafInternalHom
- Nyll.SchemeTheory.Modules.PresheafPullbackMonoidal
- Nyll.AlgebraicCurves.Foundations.Algebra.AddCommGroup_apply_zsmul_add_eq_of_forall_cube
- Nyll.AlgebraicCurves.Foundations.Algebra.AddCommGroup_exists_basis_smul_eq_of_card_torsionBy
- Nyll.AlgebraicCurves.Foundations.Algebra.AddCommGroup_exists_mem_torsionBy_smul_eq_of_card_torsionBy
- Nyll.AlgebraicCurves.Foundations.Algebra.AddCommGroup_finite_and_natCard_torsionBy_le_of_natCard_fixed_primaryComponent_le_of_divisible
- Nyll.AlgebraicCurves.Foundations.Algebra.AddCommGroup_natCard_primaryComponent_ker_aeval_of_forall_natCard_ker_aeval_eq_natAbs_resultant
- Nyll.AlgebraicCurves.Foundations.Algebra.AddCommGroup_natCard_torsionBy_pow_eq_pow_of_natCard_fixed_primaryComponent
- Nyll.AlgebraicCurves.Foundations.Algebra.AddCommGroup_nonempty_basis_zmod_pow_of_card_torsionBy
- Nyll.AlgebraicCurves.Foundations.Algebra.AddMonoidHom_exists_nsmul_eq_zero_and_apply_eq_of_surjective_of_forall_ker
- Nyll.AlgebraicCurves.Foundations.Algebra.AddMonoidHom_mem_range_of_smul_eq_zero_of_natCard_ker_mul_le_of_natCard_mul_le
- Nyll.AlgebraicCurves.Foundations.Algebra.AddMonoidHom_natCard_ker_comp_eq_mul_of_surjective
- Nyll.AlgebraicCurves.Foundations.Algebra.AlgHom_existsUnique_lift_trivSqZeroExt_of_cotangent_linearMap
- Nyll.AlgebraicCurves.Foundations.Algebra.AlgHom_exists_cotangent_linearMap_of_fst_eq
- Nyll.AlgebraicCurves.Foundations.Algebra.AlgHom_nonempty_equiv_fin_of_tensorProduct_algEquiv_pi
- Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_Etale_exists_finite_etale_faithfullyFlat_tensorProduct_algEquiv_pi
- Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_Etale_exists_finite_etale_faithfullyFlat_tensorProduct_algEquiv_pi_of_rankAtStalk_eq
- Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_FormallyEtale_of_formallySmooth_of_bijective_mapBaseChange
- Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_FormallySmooth_exists_linearMap_eq_of_symmetric_hochschild_two_cocycle
- Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_FormallySmooth_formallySmooth_and_formallyUnramified_aeval_of_existsUnique_smul_D_eq
- Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_FormallySmooth_quotient_span_singleton_of_existsUnique_eq_smul_D
- Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_IsStandardSmooth_exists_isStandardSmoothOfRelativeDimension_of_field
- Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_QuasiFinite_of_flat_of_quasiFinite_genericFiber
- Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_TensorProduct_exists_fg_subalgebra_surjective_map_of_surjective_map
- Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_TensorProduct_isDirectLimit_map_of_isDirectLimit
- Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced
- Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_algebraMap_norm_eq_norm_mul_norm_of_adjoin_eq_top
- Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_exists_algEquiv_tensorProduct_map_eq_of_finitePresentation_of_isDirectLimit
- Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_exists_algHom_tensorProduct_map_eq_of_finitePresentation_of_isDirectLimit
- Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_exists_finitePresentation_tensorProduct_algEquiv_of_isDirectLimit
- Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_exists_lift_basis_of_surjective_of_monogenic_specialFibre
- Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_exists_ne_zero_algebraicIndependent_forall_isIntegral_pow_smul_of_finiteType
- Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_exists_tensorProduct_map_apply_eq_of_finiteType_of_isDirectLimit
- Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_integralClosure_le_of_isUnit_discr_of_span_eq_top
- Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_isIntegral_trace_of_finiteDimensional
- Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_isReduced_tensorProduct_of_perfectField
- Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_isSmoothAt_of_isSmoothAt_fiber
- Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_norm_algebraMap_sub_eq_eval_minpoly_pow
- Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_norm_algebraMap_sub_eq_minpoly_eval
- Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_norm_eq_pow_finrank_of_isNilpotent_sub_algebraMap
- Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_norm_of_subsingleton
- Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_norm_one_add_eps_tmul
- Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_norm_one_tmul_eq_algebraMap_norm
- Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_norm_prod
- Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_trdeg_quotient_lt
- Nyll.AlgebraicCurves.Foundations.Algebra.Equiv_Perm_exists_comp_succAbove_eq_succAbove_comp_and_sign_eq
- Nyll.AlgebraicCurves.Foundations.Algebra.Fin_exists_forall_sub_sub_modEq_of_forall_flow_sum_mul_modEq_zero
- Nyll.AlgebraicCurves.Foundations.Algebra.Fin_exists_forall_vertexLaw_and_edgeLaw_pow_of_pow_add_of_modEq_of_forall_flow_sum_mul_eq
- Nyll.AlgebraicCurves.Foundations.Algebra.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
- Nyll.AlgebraicCurves.Foundations.Algebra.Finsupp_exists_list_eq_sum_single_sub_single_of_sum_fibre_eq_zero
- Nyll.AlgebraicCurves.Foundations.Algebra.IsAdicComplete_of_module_finite
- Nyll.AlgebraicCurves.Foundations.Algebra.LinearEquiv_exists_forall_finrank_inf_map_pow_add_finrank_inf_le
- Nyll.AlgebraicCurves.Foundations.Algebra.LinearMap_bijective_and_flip_bijective_of_baseChange_residueField
- Nyll.AlgebraicCurves.Foundations.Algebra.LinearMap_exists_ker_linearEquiv_and_quotient_linearEquiv_of_surjective_of_forall_exact
- Nyll.AlgebraicCurves.Foundations.Algebra.LinearMap_finiteDimensional_ker_and_quotient_range_of_exact_of_finiteDimensional
- Nyll.AlgebraicCurves.Foundations.Algebra.LinearMap_finrank_ker_eq_and_finrank_add_finrank_eq_of_quasiIso
- Nyll.AlgebraicCurves.Foundations.Algebra.LinearMap_finrank_ker_sub_finrank_quotient_range_eq_add_of_exact
- Nyll.AlgebraicCurves.Foundations.Algebra.LinearMap_isOpen_setOf_surjective_baseChange_residueField
- Nyll.AlgebraicCurves.Foundations.Algebra.LinearMap_nonempty_kerModRange_equiv_of_equiv_comm
- Nyll.AlgebraicCurves.Foundations.Algebra.LinearMap_sum_neg_one_pow_mul_finrank_eq_zero_of_exact
- Nyll.AlgebraicCurves.Foundations.Algebra.LinearMap_sum_roots_charpoly_map_pow_eq_trace_pow
- Nyll.AlgebraicCurves.Foundations.Algebra.Matrix_exists_transpose_mul_mul_eq_J
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_FaithfullyFlat_exists_submodule_isBaseChange_of_cocycle
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_Flat_bijective_kerBaseChangeHom_and_nonempty_homology_baseChange_linearEquiv
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_Flat_exists_fg_subalgebra_flat_tensorProduct
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_Flat_exists_forall_isUnit_ker_baseChange_le_range_of_ker_baseChange_residueField_le_range
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_Flat_exists_forall_isUnit_projective_ker_baseChange_of_ker_baseChange_residueField_le_range
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_Flat_flat_ker_and_bijective_kerBaseChangeHom_of_forall_ker_le_range
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_Flat_ker_baseChange_eq_bot_and_ker_le_range_of_flat_of_exact
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_Flat_ker_baseChange_le_range_of_forall_ker_baseChange_residueField_le_range
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_Flat_ker_le_range_of_forall_isMaximal_ker_baseChange_quotient_le_range
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_Flat_of_finitePresentation_of_forall_flat_residueField_tensorProduct
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_Flat_projective_ker_and_bijective_kerBaseChangeHom_of_forall_ker_baseChange_le_range
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_Invertible_of_projective_of_forall_finrank_eq_one
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_Invertible_of_ringEquiv
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_IsDirectLimit_exists_invertible_linearEquiv_baseChange
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_IsDirectLimit_exists_stage_linearEquiv_of_finitePresentation_compat
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_Projective_exists_baseChange_quotient_iso_of_squareZero
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_Projective_exists_linearEquiv_of_baseChange_quotient_of_squareZero_of_compat
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_Projective_nonempty_linearEquiv_of_baseChange_quotient_of_squareZero
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_depth_quotient_eq_depth
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_exists_forall_isUnit_rankAtStalk_baseChange_eq_finrank_residueField_tensor
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_exists_forall_isUnit_surjective_baseChange_of_surjective_baseChange_residueField
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_exists_forall_notMem_and_linearIndependent_and_smul_mem_span_of_finrank_baseChange_eq
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_finitePresentation_of_rankAtStalk_eq
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_finite_projective_ker_baseChange_of_forall_exists_isUnit
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_finrank_baseChange_eq_of_quotient_squareZero_linearEquiv
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_finrank_baseChange_eq_one_of_rankAtStalk_eq_one
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_flat_of_isLocalHom_of_finite_of_isZero_tor_one_residueField
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_free_and_finrank_tensorProduct_quot_span_tmul_pow_sub_eq_mul
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_free_coker_and_ker_baseChange_of_ker_le_range_residueField
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_free_quotient_range_of_ker_baseChange_residueField_le
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_isClosed_setOf_le_finrank_cohomology_baseChange_residueField_of_projective
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_ker_baseChange_field_of_subsingleton_H1
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_ker_baseChange_field_of_subsingleton_H1_of_projective
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_ker_baseChange_le_range_and_finrank_eq_of_field_extension
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_projective_of_isReduced_of_finrank_fiber_const
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_quasiIso_baseChange_of_quasiIso_of_flat
- Nyll.AlgebraicCurves.Foundations.Algebra.Module_rankAtStalk_eq_of_forall_localizedModule_equiv
- Nyll.AlgebraicCurves.Foundations.Algebra.MonoidHom_exists_subfield_units_coe_eq
- Nyll.AlgebraicCurves.Foundations.Algebra.MonoidHom_map_transfer_eq_transfer_comp
- Nyll.AlgebraicCurves.Foundations.Algebra.MulAction_ncard_orbit_inter_orbit_mul_card
- Nyll.AlgebraicCurves.Foundations.Algebra.Multiset_filter_ne_zero_eq_of_forall_prod_one_sub_pow_eq
- Nyll.AlgebraicCurves.Foundations.Algebra.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
- Nyll.AlgebraicCurves.Foundations.Algebra.Nat_macaulayPow_add_add_le_macaulayPow_add_of_le_add
- Nyll.AlgebraicCurves.Foundations.Algebra.Nat_macaulayPow_lt_macaulayPow_of_lt
- Nyll.SchemeTheory.Modules.SheafificationMonoidal
- Nyll.SchemeTheory.Modules.InternalHomSheaf
- Nyll.AlgebraicCurves.Foundations.Algebra.RatFunc_exists_algEquiv_apply_X_eq_moebius
- Nyll.AlgebraicCurves.Foundations.Algebra.RingHom_QuasiFinite_codescendsAlong_faithfullyFlat
- Nyll.AlgebraicCurves.Foundations.Algebra.RingHom_finiteDimensional_adjoin_range_of_finite_of_forall_mem_range
- Nyll.AlgebraicCurves.Foundations.Algebra.RingHom_formallySmooth_and_formallyUnramified_eval2RingHom_of_existsUnique_eq_smul_D
- Nyll.AlgebraicCurves.Foundations.Algebra.RingHom_formallySmooth_and_formallyUnramified_of_directed_union
- Nyll.AlgebraicCurves.Foundations.Algebra.RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
- Nyll.AlgebraicCurves.Foundations.Algebra.Subalgebra_fg_restrictScalars_and_le_of_fg
- Nyll.AlgebraicCurves.Foundations.Algebra.Subgroup_IsArithmetic_exists_nat_mem_strictPeriods_conj
- Nyll.AlgebraicCurves.Foundations.Algebra.Subgroup_exists_eq_mul_of_index_inf_eq
- Nyll.AlgebraicCurves.Foundations.Algebra.Submodule_finite_torsionBy_pow_of_finite_torsionBy
- Nyll.AlgebraicCurves.Foundations.Algebra.Submodule_natCard_torsionBy_quotient_eq_pow_finrank
- Nyll.AlgebraicCurves.Foundations.Algebra.SubtractionMonoid_exists_zsmul_eq_of_forall_prime
- Nyll.AlgebraicCurves.Foundations.Algebra.SubtractionMonoid_exists_zsmul_eq_of_forall_prime_nsmul
- Nyll.AlgebraicCurves.Foundations.Algebra.Tuple_succAbove_sort_comp_succAbove_eq
- Nyll.AlgebraicCurves.Foundations.Algebra.ZMod_chordMatrix_transpose_eq_neg
- Nyll.AlgebraicCurves.Foundations.Algebra.card_torsion_mul_of_divisible
- Nyll.AlgebraicCurves.Foundations.Algebra.exteriorPower_iotaMulti_comp_eq_det_smul
- Nyll.AlgebraicCurves.Foundations.Algebra.exteriorPower_map_apply_eq_det_smul
- Nyll.AlgebraicCurves.Foundations.Algebra.exteriorPower_map_mulLeft_apply_eq_norm_smul
- Nyll.SchemeTheory.Modules.Monoidal
- Nyll.AlgebraicCurves.Foundations.Algebra.SheafOfModules_MonoidalV2
- Nyll.AlgebraicCurves.Foundations.Algebra.Submodule_FiniteAdeleBox
Imported by1
This module has no indexed declarations. Its imports and full source are available here.