| Name | Category | Theorems |
|---|
AlgebraicIndepOn 📖 | MathDef | 12 mathmath: AlgebraicIndepOn.mono, AlgebraicIndependent.matroid_indep_iff, AlgebraicIndependent.iff_adjoin_image_compl, AlgebraicIndependent.matroid_isBasis_iff, isTranscendenceBasis_iff_maximal, exists_maximal_algebraicIndependent, instNonemptySubtypeSetAlgebraicIndepOnIdOfFaithfulSMul, AlgebraicIndepOn.insert_iff, AlgebraicIndepOn.insert, isEmpty_algebraicIndependent, AlgebraicIndependent.iff_adjoin_image, AlgebraicIndepOn.univ
|
AlgebraicIndependent 📖 | MathDef | 72 mathmath: algebraicIndependent_of_finite_type, AlgebraicIndependent.of_aeval, algebraicIndependent_adjoin, algebraicIndependent_sUnion_of_directed, algebraicIndependent_iff_ker_eq_bot, algebraicIndependent_of_finite_type', algebraicIndependent_of_set_of_finite, algebraicIndependent_of_finite', AlgebraicIndependent.restrict_of_comp_subtype, AlgebraicIndependent.polynomial_aeval_of_transcendental, AlgebraicIndependent.comp, AlgebraicIndependent.iff_adjoin_image_compl, algebraicIndependent_ringHom_iff_of_comp_eq, algebraicIndependent_empty_iff, AlgebraicIndependent.adjoin_iff_disjoint, AlgebraicIndependent.map', AlgebraicIndependent.coe_range, MvPolynomial.algebraicIndependent_polynomial_aeval_X, AlgebraicIndependent.sumElim_iff, AlgebraicIndependent.adjoin_of_disjoint, AlgebraicIndependent.of_ringHom_of_comp_eq, AlgebraicIndependent.lift_reprField, AlgebraicIndependent.subalgebraAlgebraicClosure, algebraicIndependent_subtype_range, AlgebraicIndependent.aeval_of_algebraicIndependent, AlgebraicIndependent.sumElim, AlgebraicIndependent.of_subtype_range, algebraicIndependent_equiv', algebraicIndependent_iff, AlgebraicIndependent.extendScalars_of_isIntegral, algebraicIndependent_iUnion_of_directed, AlgebraicIndependent.mono, AlgebraicIndependent.map, AlgebraicIndependent.option_iff_transcendental, AlgebraicIndependent.sumElim_of_tower, algebraicIndependent_iff_injective_aeval, AlgebraicIndependent.liftAlgHom_comp_reprField, algebraicIndependent_singleton_iff, AlgebraicIndependent.sumElim_comp, AlgHom.algebraicIndependent_iff, AlgebraicIndependent.image_of_comp, algebraicIndependent_subtype, MvPolynomial.algebraicIndependent_X, AlgebraicIndependent.aevalEquivField_apply_coe, AlgebraicIndependent.restrictScalars, AlgebraicIndependent.option_iff, algebraicIndependent_equiv, AlgebraicIndependent.integralClosure, algebraicIndependent_empty_type, AlgebraicIndependent.algebraicClosure, algebraicIndependent_empty, AlgebraicIndependent.of_subsingleton, algebraicIndependent_iff_transcendental, AlgebraicIndependent.iff_adjoin_image, IntermediateField.algebraicIndependent_adjoin_iff, algebraicIndependent_finset_map_embedding_subtype, algebraicIndependent_of_finite, AlgebraicIndependent.to_subtype_range', AlgebraicIndependent.image, Algebra.IsAlgebraic.algebraicIndependent_iff, AlgebraicIndependent.ringHom_of_comp_eq, algebraicIndependent_comp_subtype, Algebra.IsIntegral.algebraicIndependent_iff, AlgebraicIndependent.iff_transcendental_adjoin_image, algebraicIndependent_image, isTranscendenceBasis_iff_algebraicIndependent_isAlgebraic, AlgebraicIndependent.of_comp, algebraicIndependent_empty_type_iff, AlgebraicIndependent.extendScalars, algebraicIndependent_unique_type_iff, AlgebraicIndepOn.univ, AlgebraicIndependent.to_subtype_range
|
IsTranscendenceBasis 📖 | MathDef | 51 mathmath: AlgebraicIndependent.isTranscendenceBasis_iff_isAlgebraic, AlgEquiv.isTranscendenceBasis_iff, IsTranscendenceBasis.of_subtype_range, exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow', isTranscendenceBasis_iff_of_subsingleton, AlgEquiv.isTranscendenceBasis, IsTranscendenceBasis.to_subtype_range', isTranscendenceBasis_iff_maximal, exists_isTranscendenceBasis, IsTranscendenceBasis.of_comp_algebraMap, IntermediateField.exists_finset_maximalFor_isTranscendenceBasis_separableClosure, IsTranscendenceBasis.of_isAlgebraic_adjoin_insert_diff, isTranscendenceBasis_equiv, Algebra.IsAlgebraic.isTranscendenceBasis_iff, AlgebraicIndependent.isTranscendenceBasis_of_lift_trdeg_le_of_finite, Algebra.IsAlgebraic.isTranscendenceBasis_of_lift_le_trdeg, isTranscendenceBasis_subtype_range, AlgebraicIndependent.isTranscendenceBasis_of_trdeg_le, exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_essFiniteType, AlgebraicIndependent.matroid_isBase_iff, trdeg_eq_iSup_cardinalMk_isTranscendenceBasis, IsTranscendenceBasis.of_comp, exists_isTranscendenceBasis_superset, IntermediateField.isTranscendenceBasis_adjoin_iff, exists_isTranscendenceBasis', exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_adjoin_eq_top, isAlgebraic_iff_exists_isTranscendenceBasis_subset, IsTranscendenceBasis.comp_equiv, exists_isTranscendenceBasis_and_isSeparable_of_perfectField, Algebra.IsAlgebraic.isTranscendenceBasis_of_le_trdeg_of_finite, AlgebraicIndependent.isTranscendenceBasis_of_trdeg_le_of_finite, IsTranscendenceBasis.of_isAlgebraic_adjoin_image_compl, IsTranscendenceBasis.to_subtype_range, IsTranscendenceBasis.mvPolynomial, isTranscendenceBasis_equiv', IsTranscendenceBasis.mvPolynomial', IsTranscendenceBasis.sumElim_comp, exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow, IsTranscendenceBasis.algebraMap_comp, IsTranscendenceBasis.of_subsingleton, Algebra.IsIntegral.isTranscendenceBasis_iff, AlgebraicIndependent.isTranscendenceBasis_iff, Algebra.IsAlgebraic.isTranscendenceBasis_of_le_trdeg, Algebra.IsAlgebraic.isTranscendenceBasis_of_lift_le_trdeg_of_finite, IntermediateField.FG.exists_finset_maximalFor_isTranscendenceBasis_separableClosure, exists_isTranscendenceBasis_between, isTranscendenceBasis_iff_algebraicIndependent_isAlgebraic, IsTranscendenceBasis.polynomial, isTranscendenceBasis_image, exists_isTranscendenceBasis_subset, AlgebraicIndependent.isTranscendenceBasis_of_lift_trdeg_le
|