Documentation Verification Report

Defs

📁 Source: Mathlib/RingTheory/AlgebraicIndependent/Defs.lean

Statistics

Metric	Count
Definitions `AlgebraicIndepOn`, `aevalEquiv`, `AlgebraicIndependent`, `aevalEquiv`, `repr`, `IsTranscendenceBasis`	6
Theorems `mono`, `univ`, `aevalEquiv_apply_coe`, `aeval_comp_repr`, `aeval_repr`, `algebraMap_aevalEquiv`, `coe_range`, `comp`, `eq_zero_of_aeval_eq_zero`, `mono`, `of_comp`, `of_subtype_range`, `comp_equiv`, `of_subtype_range`, `algebraicIndependent_equiv`, `algebraicIndependent_equiv'`, `algebraicIndependent_iff`, `algebraicIndependent_iff_injective_aeval`, `algebraicIndependent_image`, `algebraicIndependent_subtype_range`, `isTranscendenceBasis_equiv`, `isTranscendenceBasis_equiv'`, `isTranscendenceBasis_iff_maximal`, `isTranscendenceBasis_image`, `isTranscendenceBasis_subtype_range`	25
Total	31

AlgebraicIndepOn

Definitions

Name	Category	Theorems
`aevalEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mono` 📖	—	`AlgebraicIndepOn` `Set` `Set.instHasSubset`	—	—	`AlgebraicIndependent.comp` `Set.inclusion_injective`
`univ` 📖	mathematical	—	`AlgebraicIndepOn` `Set.univ` `AlgebraicIndependent`	—	`algebraicIndependent_equiv`

AlgebraicIndependent

Definitions

Name	Category	Theorems
`aevalEquiv` 📖	CompOp	5 math math: `mvPolynomialOptionEquivPolynomialAdjoin_C'`, `mvPolynomialOptionEquivPolynomialAdjoin_X_some`, `mvPolynomialOptionEquivPolynomialAdjoin_apply`, `algebraMap_aevalEquiv`, `aevalEquiv_apply_coe`
`repr` 📖	CompOp	3 math math: `repr_ker`, `aeval_comp_repr`, `aeval_repr`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aevalEquiv_apply_coe` 📖	mathematical	`AlgebraicIndependent`	`Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.range` `DFunLike.coe` `AlgEquiv` `MvPolynomial` `MvPolynomial.commSemiring` `Subalgebra.toSemiring` `MvPolynomial.algebra` `Algebra.id` `Subalgebra.algebra` `AlgEquiv.instFunLike` `aevalEquiv` `AlgHom` `AlgHom.funLike` `MvPolynomial.aeval`	—	—
`aeval_comp_repr` 📖	mathematical	`AlgebraicIndependent`	`AlgHom.comp` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.range` `MvPolynomial` `Subalgebra.toSemiring` `MvPolynomial.commSemiring` `Subalgebra.algebra` `MvPolynomial.algebra` `Algebra.id` `MvPolynomial.aeval` `repr` `Subalgebra.val`	—	`AlgHom.ext` `aeval_repr`
`aeval_repr` 📖	mathematical	`AlgebraicIndependent`	`DFunLike.coe` `AlgHom` `MvPolynomial` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike` `MvPolynomial.aeval` `Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.range` `Subalgebra.toSemiring` `Subalgebra.algebra` `repr`	—	`AlgEquiv.apply_symm_apply`
`algebraMap_aevalEquiv` 📖	mathematical	`AlgebraicIndependent`	`DFunLike.coe` `RingHom` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set.range` `Semiring.toNonAssocSemiring` `Subalgebra.toCommSemiring` `RingHom.instFunLike` `algebraMap` `Subalgebra.toAlgebra` `Algebra.id` `AlgEquiv` `MvPolynomial` `MvPolynomial.commSemiring` `Subalgebra.toSemiring` `MvPolynomial.algebra` `Subalgebra.algebra` `AlgEquiv.instFunLike` `aevalEquiv` `AlgHom` `AlgHom.funLike` `MvPolynomial.aeval`	—	—
`coe_range` 📖	mathematical	`AlgebraicIndependent`	`Set` `Set.instMembership` `Set.range`	—	`Set.comp_rangeSplitting` `comp` `Set.rangeSplitting_injective`
`comp` 📖	—	`AlgebraicIndependent`	—	—	`MvPolynomial.aeval_rename` `MvPolynomial.rename_injective`
`eq_zero_of_aeval_eq_zero` 📖	mathematical	`AlgebraicIndependent` `DFunLike.coe` `AlgHom` `MvPolynomial` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike` `MvPolynomial.aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`MvPolynomial.instCommRingMvPolynomial`	—	`algebraicIndependent_iff`
`mono` 📖	—	`Set` `Set.instHasSubset` `AlgebraicIndependent` `Set.instMembership`	—	—	`AlgebraicIndepOn.mono`
`of_comp` 📖	—	`AlgebraicIndependent` `DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AlgHom.funLike`	—	—	`MvPolynomial.algHom_ext` `MvPolynomial.aeval_X` `Function.Injective.of_comp` `AlgHom.coe_comp` `eq_1`
`of_subtype_range` 📖	—	`AlgebraicIndependent` `Set` `Set.instMembership` `Set.range`	—	—	`algebraicIndependent_subtype_range`

IsTranscendenceBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_equiv` 📖	mathematical	`IsTranscendenceBasis`	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`isTranscendenceBasis_equiv`
`of_subtype_range` 📖	—	`IsTranscendenceBasis` `Set` `Set.instMembership` `Set.range`	—	—	`isTranscendenceBasis_subtype_range`

(root)

Definitions

Name	Category	Theorems
`AlgebraicIndepOn` 📖	MathDef	9 math math: `AlgebraicIndependent.matroid_indep_iff`, `AlgebraicIndependent.iff_adjoin_image_compl`, `AlgebraicIndependent.matroid_isBasis_iff`, `isTranscendenceBasis_iff_maximal`, `instNonemptySubtypeSetAlgebraicIndepOnIdOfFaithfulSMul`, `AlgebraicIndepOn.insert_iff`, `isEmpty_algebraicIndependent`, `AlgebraicIndependent.iff_adjoin_image`, `AlgebraicIndepOn.univ`
`AlgebraicIndependent` 📖	MathDef	33 math math: `algebraicIndependent_iff_ker_eq_bot`, `algebraicIndependent_of_finite_type'`, `algebraicIndependent_of_finite'`, `AlgebraicIndependent.iff_adjoin_image_compl`, `algebraicIndependent_ringHom_iff_of_comp_eq`, `algebraicIndependent_empty_iff`, `MvPolynomial.algebraicIndependent_polynomial_aeval_X`, `AlgebraicIndependent.sumElim_iff`, `algebraicIndependent_subtype_range`, `algebraicIndependent_equiv'`, `algebraicIndependent_iff`, `algebraicIndependent_iff_injective_aeval`, `algebraicIndependent_singleton_iff`, `AlgHom.algebraicIndependent_iff`, `algebraicIndependent_subtype`, `MvPolynomial.algebraicIndependent_X`, `AlgebraicIndependent.option_iff`, `algebraicIndependent_equiv`, `algebraicIndependent_empty_type`, `algebraicIndependent_empty`, `AlgebraicIndependent.of_subsingleton`, `algebraicIndependent_iff_transcendental`, `AlgebraicIndependent.iff_adjoin_image`, `IntermediateField.algebraicIndependent_adjoin_iff`, `Algebra.IsAlgebraic.algebraicIndependent_iff`, `algebraicIndependent_comp_subtype`, `Algebra.IsIntegral.algebraicIndependent_iff`, `AlgebraicIndependent.iff_transcendental_adjoin_image`, `algebraicIndependent_image`, `isTranscendenceBasis_iff_algebraicIndependent_isAlgebraic`, `algebraicIndependent_empty_type_iff`, `algebraicIndependent_unique_type_iff`, `AlgebraicIndepOn.univ`
`IsTranscendenceBasis` 📖	MathDef	37 math math: `AlgebraicIndependent.isTranscendenceBasis_iff_isAlgebraic`, `AlgEquiv.isTranscendenceBasis_iff`, `isTranscendenceBasis_iff_of_subsingleton`, `isTranscendenceBasis_iff_maximal`, `exists_isTranscendenceBasis`, `IntermediateField.exists_finset_maximalFor_isTranscendenceBasis_separableClosure`, `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`, `exists_isTranscendenceBasis_superset`, `IntermediateField.isTranscendenceBasis_adjoin_iff`, `exists_isTranscendenceBasis'`, `isAlgebraic_iff_exists_isTranscendenceBasis_subset`, `exists_isTranscendenceBasis_and_isSeparable_of_perfectField`, `Algebra.IsAlgebraic.isTranscendenceBasis_of_le_trdeg_of_finite`, `AlgebraicIndependent.isTranscendenceBasis_of_trdeg_le_of_finite`, `IsTranscendenceBasis.mvPolynomial`, `isTranscendenceBasis_equiv'`, `IsTranscendenceBasis.mvPolynomial'`, `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`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraicIndependent_equiv` 📖	mathematical	—	`AlgebraicIndependent` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`AlgebraicIndependent.comp` `Equiv.injective` `Equiv.self_comp_symm`
`algebraicIndependent_equiv'` 📖	mathematical	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	`AlgebraicIndependent`	—	`algebraicIndependent_equiv`
`algebraicIndependent_iff` 📖	mathematical	—	`AlgebraicIndependent` `MvPolynomial` `CommRing.toCommSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MvPolynomial.instCommRingMvPolynomial`	—	`injective_iff_map_eq_zero` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass`
`algebraicIndependent_iff_injective_aeval` 📖	mathematical	—	`AlgebraicIndependent` `MvPolynomial` `CommRing.toCommSemiring` `DFunLike.coe` `AlgHom` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike` `MvPolynomial.aeval`	—	—
`algebraicIndependent_image` 📖	mathematical	`Set.InjOn`	`AlgebraicIndependent` `Set.Elem` `Set` `Set.instMembership` `Set.image`	—	`algebraicIndependent_equiv'`
`algebraicIndependent_subtype_range` 📖	mathematical	—	`AlgebraicIndependent` `Set` `Set.instMembership` `Set.range`	—	`algebraicIndependent_equiv'`
`isTranscendenceBasis_equiv` 📖	mathematical	—	`IsTranscendenceBasis` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`EquivLike.range_comp`
`isTranscendenceBasis_equiv'` 📖	mathematical	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	`IsTranscendenceBasis`	—	`isTranscendenceBasis_equiv`
`isTranscendenceBasis_iff_maximal` 📖	mathematical	—	`IsTranscendenceBasis` `Set` `Set.instMembership` `Maximal` `Set.instLE` `AlgebraicIndepOn`	—	`IsTranscendenceBasis.eq_1` `maximal_iff` `Subtype.range_val`
`isTranscendenceBasis_image` 📖	mathematical	`Set.InjOn`	`IsTranscendenceBasis` `Set.Elem` `Set` `Set.instMembership` `Set.image`	—	`isTranscendenceBasis_equiv'`
`isTranscendenceBasis_subtype_range` 📖	mathematical	—	`IsTranscendenceBasis` `Set` `Set.instMembership` `Set.range`	—	`isTranscendenceBasis_equiv'`

---

← Back to Index