Core

📁 Source: Mathlib/RingTheory/Extension/Presentation/Core.lean

Statistics

Metric	Count
Definitions ofHasCoeffs, Core, HasCoeffs, ModelOfHasCoeffs, coeffs, core, instCommRingCore, instCore, instCore_1, relationOfHasCoeffs, tensorModelOfHasCoeffsEquiv, tensorModelOfHasCoeffsHom, tensorModelOfHasCoeffsInv, HasCoeffs, coeffs, invJacobianOfHasCoeffs, jacobianOfHasCoeffs, jacobianRelations, jacobianRelationsOfHasCoeffs, ofHasCoeffs	20
Theorems ofHasCoeffs_algebra_algebraMap_apply, ofHasCoeffs_algebra_smul, ofHasCoeffs_map, ofHasCoeffs_relation, ofHasCoeffs_val, ofHasCoeffs_σ', coeffs_relation_mem_range, coeffs_subset_range, of_isScalarTower, relation_mem_range_map, aeval_val_relationOfHasCoeffs, algebraTensorAlgEquiv_symm_relation, coeffs_relation_subset_coeffs, coeffs_relation_subset_core, coeffs_subset_core, coeffs_subset_range, finite_coeffs, instFaithfulSMulCore, instFinitePresentationModelOfHasCoeffsOfFinite, instFiniteTypeIntCoreOfFinite, instHasCoeffsCore, instHasCoeffsSubtypeMemSubalgebraAdjoin, instIsScalarTowerCore, map_relationOfHasCoeffs, tensorModelOfHasCoeffsEquiv_symm_tmul, tensorModelOfHasCoeffsEquiv_tmul, tensorModelOfHasCoeffsHom_tmul, tensorModelOfHasCoeffsInv_aeval_val, coeffs_subset_range, aeval_invJacobianOfHasCoeffs, aeval_jacobianOfHasCoeffs, coeffs_toPresentation_subset_coeffs, exists_sum_eq_σ_jacobian_mul_σ_jacobian_inv_sub_one, finite_coeffs, instHasCoeffs, jacobianRelations_spec, map_invJacobianOfHasCoeffs, map_jacobianOfHasCoeffs, map_jacobianRelationsOfHasCoeffs, sum_jacobianRelationsOfHasCoeffs_mul_relationOfHasCoeffs	40
Total	60

Algebra.PreSubmersivePresentation

Definitions

Name	Category	Theorems
ofHasCoeffs 📖	CompOp	6 math math: ofHasCoeffs_map, ofHasCoeffs_relation, ofHasCoeffs_σ', ofHasCoeffs_algebra_algebraMap_apply, ofHasCoeffs_val, ofHasCoeffs_algebra_smul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofHasCoeffs_algebra_algebraMap_apply 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing MvPolynomial.instCommRingMvPolynomial Ideal.instHasQuotient Ideal.span CommSemiring.toSemiring MvPolynomial.commSemiring Set.range Algebra.Presentation.relationOfHasCoeffs toPresentation Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike Algebra.algebraMap Ideal.instHasQuotient_1 Ideal.Quotient.commRing Algebra.Generators.algebra Algebra.Presentation.ModelOfHasCoeffs Ideal.instAlgebraQuotient MvPolynomial.algebra Algebra.id Algebra.Presentation.toGenerators ofHasCoeffs	—	Ideal.instIsTwoSided_1
ofHasCoeffs_algebra_smul 📖	mathematical	—	MvPolynomial CommRing.toCommSemiring HasQuotient.Quotient Ideal CommSemiring.toSemiring MvPolynomial.commSemiring Ideal.instHasQuotient_1 MvPolynomial.instCommRingMvPolynomial Ideal.span Set.range Algebra.Presentation.relationOfHasCoeffs toPresentation Algebra.toSMul Ideal.Quotient.commRing Algebra.Generators.algebra Algebra.Presentation.ModelOfHasCoeffs Ideal.instAlgebraQuotient MvPolynomial.algebra Algebra.id Algebra.Presentation.toGenerators ofHasCoeffs Quotient.map' Submodule.quotientRel CommRing.toRing Ring.toAddCommGroup Semiring.toModule Ring.toSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	—
ofHasCoeffs_map 📖	mathematical	—	map Algebra.Presentation.ModelOfHasCoeffs toPresentation Ideal.Quotient.commRing MvPolynomial CommRing.toCommSemiring MvPolynomial.instCommRingMvPolynomial Ideal.span CommSemiring.toSemiring MvPolynomial.commSemiring Set.range Algebra.Presentation.relationOfHasCoeffs Ideal.instAlgebraQuotient MvPolynomial.algebra Algebra.id ofHasCoeffs	—	—
ofHasCoeffs_relation 📖	mathematical	—	Algebra.Presentation.relation Algebra.Presentation.ModelOfHasCoeffs toPresentation Ideal.Quotient.commRing MvPolynomial CommRing.toCommSemiring MvPolynomial.instCommRingMvPolynomial Ideal.span CommSemiring.toSemiring MvPolynomial.commSemiring Set.range Algebra.Presentation.relationOfHasCoeffs Ideal.instAlgebraQuotient MvPolynomial.algebra Algebra.id ofHasCoeffs	—	—
ofHasCoeffs_val 📖	mathematical	—	Algebra.Generators.val Algebra.Presentation.ModelOfHasCoeffs toPresentation Ideal.Quotient.commRing MvPolynomial CommRing.toCommSemiring MvPolynomial.instCommRingMvPolynomial Ideal.span CommSemiring.toSemiring MvPolynomial.commSemiring Set.range Algebra.Presentation.relationOfHasCoeffs Ideal.instAlgebraQuotient MvPolynomial.algebra Algebra.id Algebra.Presentation.toGenerators ofHasCoeffs DFunLike.coe RingHom HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Semiring.toNonAssocSemiring Ideal.Quotient.ring RingHom.instFunLike MvPolynomial.X	—	—
ofHasCoeffs_σ' 📖	mathematical	—	Algebra.Generators.σ' Algebra.Presentation.ModelOfHasCoeffs toPresentation Ideal.Quotient.commRing MvPolynomial CommRing.toCommSemiring MvPolynomial.instCommRingMvPolynomial Ideal.span CommSemiring.toSemiring MvPolynomial.commSemiring Set.range Algebra.Presentation.relationOfHasCoeffs Ideal.instAlgebraQuotient MvPolynomial.algebra Algebra.id Algebra.Presentation.toGenerators ofHasCoeffs Function.surjInv HasQuotient.Quotient Ideal Ideal.instHasQuotient_1 DFunLike.coe RingHom Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Semiring.toNonAssocSemiring Ideal.Quotient.ring RingHom.instFunLike	—	—

Algebra.Presentation

Definitions

Name	Category	Theorems
Core 📖	CompOp	4 math math: instIsScalarTowerCore, instFaithfulSMulCore, instHasCoeffsCore, instFiniteTypeIntCoreOfFinite
HasCoeffs 📖	CompData	4 math math: HasCoeffs.of_isScalarTower, Algebra.SubmersivePresentation.instHasCoeffs, instHasCoeffsSubtypeMemSubalgebraAdjoin, instHasCoeffsCore
ModelOfHasCoeffs 📖	CompOp	11 math math: Algebra.PreSubmersivePresentation.ofHasCoeffs_map, Algebra.PreSubmersivePresentation.ofHasCoeffs_relation, Algebra.PreSubmersivePresentation.ofHasCoeffs_σ', Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_algebraMap_apply, tensorModelOfHasCoeffsEquiv_tmul, tensorModelOfHasCoeffsHom_tmul, instFinitePresentationModelOfHasCoeffsOfFinite, tensorModelOfHasCoeffsEquiv_symm_tmul, Algebra.PreSubmersivePresentation.ofHasCoeffs_val, Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_smul, tensorModelOfHasCoeffsInv_aeval_val
coeffs 📖	CompOp	6 math math: coeffs_relation_subset_coeffs, coeffs_subset_core, Algebra.SubmersivePresentation.coeffs_toPresentation_subset_coeffs, coeffs_subset_range, HasCoeffs.coeffs_subset_range, finite_coeffs
core 📖	CompOp	2 math math: coeffs_subset_core, coeffs_relation_subset_core
instCommRingCore 📖	CompOp	4 math math: instIsScalarTowerCore, instFaithfulSMulCore, instHasCoeffsCore, instFiniteTypeIntCoreOfFinite
instCore 📖	CompOp	3 math math: instIsScalarTowerCore, instFaithfulSMulCore, instHasCoeffsCore
instCore_1 📖	CompOp	2 math math: instIsScalarTowerCore, instHasCoeffsCore
relationOfHasCoeffs 📖	CompOp	15 math math: Algebra.PreSubmersivePresentation.ofHasCoeffs_map, Algebra.PreSubmersivePresentation.ofHasCoeffs_relation, Algebra.PreSubmersivePresentation.ofHasCoeffs_σ', map_relationOfHasCoeffs, Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_algebraMap_apply, tensorModelOfHasCoeffsEquiv_tmul, tensorModelOfHasCoeffsHom_tmul, Algebra.SubmersivePresentation.sum_jacobianRelationsOfHasCoeffs_mul_relationOfHasCoeffs, aeval_val_relationOfHasCoeffs, instFinitePresentationModelOfHasCoeffsOfFinite, algebraTensorAlgEquiv_symm_relation, tensorModelOfHasCoeffsEquiv_symm_tmul, Algebra.PreSubmersivePresentation.ofHasCoeffs_val, Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_smul, tensorModelOfHasCoeffsInv_aeval_val
tensorModelOfHasCoeffsEquiv 📖	CompOp	2 math math: tensorModelOfHasCoeffsEquiv_tmul, tensorModelOfHasCoeffsEquiv_symm_tmul
tensorModelOfHasCoeffsHom 📖	CompOp	1 math math: tensorModelOfHasCoeffsHom_tmul
tensorModelOfHasCoeffsInv 📖	CompOp	1 math math: tensorModelOfHasCoeffsInv_aeval_val

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeval_val_relationOfHasCoeffs 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike MvPolynomial.aeval Algebra.Generators.val toGenerators relationOfHasCoeffs MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	MvPolynomial.aeval_map_algebraMap map_relationOfHasCoeffs aeval_val_relation
algebraTensorAlgEquiv_symm_relation 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial CommRing.toCommSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring Algebra.toModule MvPolynomial.module Semiring.toModule Algebra.TensorProduct.instSemiring MvPolynomial.algebra Algebra.id Algebra.TensorProduct.leftAlgebra Algebra.to_smulCommClass AlgEquiv.instFunLike AlgEquiv.symm MvPolynomial.algebraTensorAlgEquiv relation TensorProduct.tmul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MvPolynomial.instCommRingMvPolynomial AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing relationOfHasCoeffs	—	Algebra.to_smulCommClass map_relationOfHasCoeffs MvPolynomial.algebraTensorAlgEquiv_symm_map
coeffs_relation_subset_coeffs 📖	mathematical	—	Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike MvPolynomial.coeffs CommRing.toCommSemiring relation coeffs	—	Set.subset_iUnion_of_subset Set.instReflSubset
coeffs_relation_subset_core 📖	mathematical	—	Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike MvPolynomial.coeffs CommRing.toCommSemiring relation Subalgebra Int.instCommSemiring CommSemiring.toSemiring Ring.toIntAlgebra CommRing.toRing Subalgebra.instSetLike core	—	subset_trans Set.instIsTransSubset coeffs_relation_subset_coeffs coeffs_subset_core
coeffs_subset_core 📖	mathematical	—	Set Set.instHasSubset coeffs SetLike.coe Subalgebra Int.instCommSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ring.toIntAlgebra CommRing.toRing Subalgebra.instSetLike core	—	Algebra.subset_adjoin
coeffs_subset_range 📖	mathematical	—	Set Set.instHasSubset coeffs Set.range DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	—	HasCoeffs.coeffs_subset_range
finite_coeffs 📖	mathematical	—	Set.Finite coeffs	—	Set.finite_iUnion Finset.finite_toSet
instFaithfulSMulCore 📖	mathematical	—	FaithfulSMul Core Algebra.toSMul CommRing.toCommSemiring instCommRingCore CommSemiring.toSemiring instCore	—	Subalgebra.instFaithfulSMulSubtypeMem instFaithfulSMul
instFinitePresentationModelOfHasCoeffsOfFinite 📖	mathematical	—	Algebra.FinitePresentation ModelOfHasCoeffs CommRing.toCommSemiring Ideal.Quotient.semiring MvPolynomial MvPolynomial.instCommRingMvPolynomial Ideal.span CommSemiring.toSemiring MvPolynomial.commSemiring Set.range relationOfHasCoeffs Ideal.instAlgebraQuotient MvPolynomial.algebra Algebra.id	—	nonempty_fintype Algebra.FinitePresentation.quotient Finset.coe_image Finset.coe_univ Set.image_univ Algebra.FinitePresentation.mvPolynomial Algebra.FinitePresentation.self
instFiniteTypeIntCoreOfFinite 📖	mathematical	—	Algebra.FiniteType Core Int.instCommSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRingCore Ring.toIntAlgebra CommRing.toRing	—	Algebra.FiniteType.adjoin_of_finite finite_coeffs
instHasCoeffsCore 📖	mathematical	—	HasCoeffs Core instCommRingCore instCore instCore_1 instIsScalarTowerCore	—	instIsScalarTowerCore subset_trans Set.instIsTransSubset coeffs_subset_core AlgHomClass.toRingHomClass AlgHom.algHomClass RingHomCompTriple.comp_eq RingHomCompTriple.right_ids Subtype.range_coe_subtype Set.instReflSubset
instHasCoeffsSubtypeMemSubalgebraAdjoin 📖	mathematical	—	HasCoeffs Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike Algebra.adjoin Subalgebra.toCommRing Subalgebra.toAlgebra Algebra.id IsScalarTower.subalgebra	—	HasCoeffs.of_isScalarTower IsScalarTower.subalgebra' IsScalarTower.right IsScalarTower.subalgebra
instIsScalarTowerCore 📖	mathematical	—	IsScalarTower Core Algebra.toSMul CommRing.toCommSemiring instCommRingCore CommSemiring.toSemiring instCore instCore_1	—	IsScalarTower.subalgebra
map_relationOfHasCoeffs 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.map algebraMap relationOfHasCoeffs relation	—	HasCoeffs.relation_mem_range_map
tensorModelOfHasCoeffsEquiv_symm_tmul 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct CommRing.toCommSemiring ModelOfHasCoeffs NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing MvPolynomial MvPolynomial.instCommRingMvPolynomial Ideal.span CommSemiring.toSemiring MvPolynomial.commSemiring Set.range relationOfHasCoeffs Algebra.toModule Submodule.Quotient.module' CommRing.toRing Ring.toAddCommGroup Semiring.toModule Algebra.toSMul MvPolynomial.algebra Algebra.id MvPolynomial.module IsScalarTower.right Algebra.TensorProduct.instSemiring Ideal.Quotient.semiring Ideal.instAlgebraQuotient Algebra.TensorProduct.leftAlgebra Algebra.to_smulCommClass AlgEquiv.instFunLike AlgEquiv.symm tensorModelOfHasCoeffsEquiv AlgHom AlgHom.funLike MvPolynomial.aeval Algebra.Generators.val toGenerators TensorProduct.tmul HasQuotient.Quotient Ideal Ring.toSemiring Ideal.instHasQuotient AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne RingHom Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike	—	tensorModelOfHasCoeffsInv_aeval_val
tensorModelOfHasCoeffsEquiv_tmul 📖	mathematical	—	DFunLike.coe AlgEquiv TensorProduct CommRing.toCommSemiring ModelOfHasCoeffs NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing MvPolynomial MvPolynomial.instCommRingMvPolynomial Ideal.span CommSemiring.toSemiring MvPolynomial.commSemiring Set.range relationOfHasCoeffs Algebra.toModule Submodule.Quotient.module' CommRing.toRing Ring.toAddCommGroup Semiring.toModule Algebra.toSMul MvPolynomial.algebra Algebra.id MvPolynomial.module IsScalarTower.right Algebra.TensorProduct.instSemiring Ideal.Quotient.semiring Ideal.instAlgebraQuotient Algebra.TensorProduct.leftAlgebra Algebra.to_smulCommClass AlgEquiv.instFunLike tensorModelOfHasCoeffsEquiv TensorProduct.tmul RingHom HasQuotient.Quotient Ideal Ring.toSemiring Ideal.instHasQuotient Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib algebraMap AlgHom AlgHom.funLike MvPolynomial.aeval Algebra.Generators.val toGenerators	—	IsScalarTower.right Algebra.to_smulCommClass Ideal.instIsTwoSided_1
tensorModelOfHasCoeffsHom_tmul 📖	mathematical	—	DFunLike.coe AlgHom TensorProduct CommRing.toCommSemiring ModelOfHasCoeffs NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing MvPolynomial MvPolynomial.instCommRingMvPolynomial Ideal.span CommSemiring.toSemiring MvPolynomial.commSemiring Set.range relationOfHasCoeffs Algebra.toModule Submodule.Quotient.module' CommRing.toRing Ring.toAddCommGroup Semiring.toModule Algebra.toSMul MvPolynomial.algebra Algebra.id MvPolynomial.module IsScalarTower.right Algebra.TensorProduct.instSemiring Ideal.Quotient.semiring Ideal.instAlgebraQuotient Algebra.TensorProduct.leftAlgebra Algebra.to_smulCommClass AlgHom.funLike tensorModelOfHasCoeffsHom TensorProduct.tmul RingHom HasQuotient.Quotient Ideal Ring.toSemiring Ideal.instHasQuotient Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib algebraMap MvPolynomial.aeval Algebra.Generators.val toGenerators	—	IsScalarTower.right Algebra.to_smulCommClass Ideal.instIsTwoSided_1
tensorModelOfHasCoeffsInv_aeval_val 📖	mathematical	—	DFunLike.coe AlgHom TensorProduct CommRing.toCommSemiring ModelOfHasCoeffs NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing MvPolynomial MvPolynomial.instCommRingMvPolynomial Ideal.span CommSemiring.toSemiring MvPolynomial.commSemiring Set.range relationOfHasCoeffs Algebra.toModule Submodule.Quotient.module' CommRing.toRing Ring.toAddCommGroup Semiring.toModule Algebra.toSMul MvPolynomial.algebra Algebra.id MvPolynomial.module IsScalarTower.right Algebra.TensorProduct.instSemiring Ideal.Quotient.semiring Ideal.instAlgebraQuotient Algebra.TensorProduct.leftAlgebra Algebra.to_smulCommClass AlgHom.funLike tensorModelOfHasCoeffsInv MvPolynomial.aeval Algebra.Generators.val toGenerators TensorProduct.tmul HasQuotient.Quotient Ideal Ring.toSemiring Ideal.instHasQuotient AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne RingHom Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike	—	IsScalarTower.right Algebra.to_smulCommClass Ideal.instIsTwoSided_1 MvPolynomial.aeval_map_algebraMap Algebra.Generators.algebraMap_apply AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass AlgEquiv.symm_apply_apply MvPolynomial.algebraTensorAlgEquiv_symm_map

Algebra.Presentation.HasCoeffs

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeffs_relation_mem_range 📖	mathematical	—	Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike MvPolynomial.coeffs CommRing.toCommSemiring Algebra.Presentation.relation Set.range DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	subset_trans Set.instIsTransSubset Algebra.Presentation.coeffs_relation_subset_coeffs coeffs_subset_range
coeffs_subset_range 📖	mathematical	—	Set Set.instHasSubset Algebra.Presentation.coeffs Set.range DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	—	—
of_isScalarTower 📖	mathematical	—	Algebra.Presentation.HasCoeffs	—	subset_trans Set.instIsTransSubset Algebra.Presentation.coeffs_subset_range IsScalarTower.algebraMap_eq Set.range_comp Set.preimage_range
relation_mem_range_map 📖	mathematical	—	Algebra.Generators.Ring Algebra.Presentation.toGenerators Set MvPolynomial CommRing.toCommSemiring Set.instMembership Set.range DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.map algebraMap Algebra.Presentation.relation	—	MvPolynomial.mem_range_map_iff_coeffs_subset coeffs_relation_mem_range

Algebra.SubmersivePresentation

Definitions

Name	Category	Theorems
HasCoeffs 📖	CompData	—
coeffs 📖	CompOp	3 math math: HasCoeffs.coeffs_subset_range, coeffs_toPresentation_subset_coeffs, finite_coeffs
invJacobianOfHasCoeffs 📖	CompOp	3 math math: map_invJacobianOfHasCoeffs, sum_jacobianRelationsOfHasCoeffs_mul_relationOfHasCoeffs, aeval_invJacobianOfHasCoeffs
jacobianOfHasCoeffs 📖	CompOp	3 math math: map_jacobianOfHasCoeffs, sum_jacobianRelationsOfHasCoeffs_mul_relationOfHasCoeffs, aeval_jacobianOfHasCoeffs
jacobianRelations 📖	CompOp	2 math math: jacobianRelations_spec, map_jacobianRelationsOfHasCoeffs
jacobianRelationsOfHasCoeffs 📖	CompOp	2 math math: map_jacobianRelationsOfHasCoeffs, sum_jacobianRelationsOfHasCoeffs_mul_relationOfHasCoeffs
ofHasCoeffs 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeval_invJacobianOfHasCoeffs 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike MvPolynomial.aeval Algebra.Generators.val Algebra.Presentation.toGenerators Algebra.PreSubmersivePresentation.toPresentation toPreSubmersivePresentation invJacobianOfHasCoeffs Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Units Units.instInv IsUnit.unit Algebra.PreSubmersivePresentation.jacobian jacobian_isUnit	—	jacobian_isUnit MvPolynomial.aeval_map_algebraMap Algebra.Generators.aeval_val_σ map_invJacobianOfHasCoeffs
aeval_jacobianOfHasCoeffs 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike MvPolynomial.aeval Algebra.Generators.val Algebra.Presentation.toGenerators Algebra.PreSubmersivePresentation.toPresentation toPreSubmersivePresentation jacobianOfHasCoeffs Algebra.PreSubmersivePresentation.jacobian	—	MvPolynomial.aeval_map_algebraMap map_jacobianOfHasCoeffs Finite.of_fintype Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det Algebra.Generators.algebraMap_apply
coeffs_toPresentation_subset_coeffs 📖	mathematical	—	Set Set.instHasSubset Algebra.Presentation.coeffs Algebra.PreSubmersivePresentation.toPresentation toPreSubmersivePresentation coeffs	—	HasSubset.Subset.trans Set.instIsTransSubset jacobian_isUnit Set.subset_union_left
exists_sum_eq_σ_jacobian_mul_σ_jacobian_inv_sub_one 📖	mathematical	—	Finset.sum MvPolynomial CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MvPolynomial.instCommRingMvPolynomial Finset.univ Algebra.Generators.Ring Algebra.Presentation.toGenerators Algebra.PreSubmersivePresentation.toPresentation toPreSubmersivePresentation Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Algebra.Presentation.relation SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Matrix.det Algebra.PreSubmersivePresentation.jacobiMatrix Algebra.Generators.σ Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Units Units.instInv IsUnit.unit Algebra.PreSubmersivePresentation.jacobian jacobian_isUnit AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	jacobian_isUnit Finite.of_fintype Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det Algebra.Generators.algebraMap_apply IsUnit.unit.congr_simp map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass map_mul NonUnitalAlgSemiHomClass.toMulHomClass Algebra.Generators.aeval_val_σ IsUnit.mul_val_inv map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass sub_self Ideal.mem_span_range_iff_exists_fun Algebra.Presentation.span_range_relation_eq_ker
finite_coeffs 📖	mathematical	—	Set.Finite coeffs	—	Set.Finite.union jacobian_isUnit Algebra.Presentation.finite_coeffs Set.Finite.iUnion Set.finite_univ instIsEmptyFalse
instHasCoeffs 📖	mathematical	—	Algebra.Presentation.HasCoeffs Algebra.PreSubmersivePresentation.toPresentation toPreSubmersivePresentation	—	HasSubset.Subset.trans Set.instIsTransSubset coeffs_toPresentation_subset_coeffs HasCoeffs.coeffs_subset_range
jacobianRelations_spec 📖	mathematical	—	Finset.sum MvPolynomial CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MvPolynomial.instCommRingMvPolynomial Finset.univ Algebra.Generators.Ring Algebra.Presentation.toGenerators Algebra.PreSubmersivePresentation.toPresentation toPreSubmersivePresentation Distrib.toMul NonUnitalNonAssocSemiring.toDistrib jacobianRelations Algebra.Presentation.relation SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Matrix.det Algebra.PreSubmersivePresentation.jacobiMatrix Algebra.Generators.σ Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Units Units.instInv IsUnit.unit Algebra.PreSubmersivePresentation.jacobian jacobian_isUnit AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	jacobian_isUnit exists_sum_eq_σ_jacobian_mul_σ_jacobian_inv_sub_one Finset.sum_congr Lean.Meta.FastSubsingleton.elim Fintype.instFastSubsingleton Lean.Meta.instFastSubsingletonForall Lean.Meta.instFastSubsingletonDecidable
map_invJacobianOfHasCoeffs 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.map algebraMap invJacobianOfHasCoeffs Algebra.Generators.σ Algebra.Presentation.toGenerators Algebra.PreSubmersivePresentation.toPresentation toPreSubmersivePresentation Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Units Units.instInv IsUnit.unit Algebra.PreSubmersivePresentation.jacobian jacobian_isUnit	—	jacobian_isUnit MvPolynomial.mem_range_map_iff_coeffs_subset HasSubset.Subset.trans Set.instIsTransSubset Set.subset_union_right Set.subset_union_left HasCoeffs.coeffs_subset_range
map_jacobianOfHasCoeffs 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.map algebraMap jacobianOfHasCoeffs Matrix.det Algebra.Generators.Ring Algebra.Presentation.toGenerators Algebra.PreSubmersivePresentation.toPresentation toPreSubmersivePresentation MvPolynomial.instCommRingMvPolynomial Algebra.PreSubmersivePresentation.jacobiMatrix	—	instHasCoeffs jacobianOfHasCoeffs.eq_1 RingHom.map_det Lean.Meta.FastSubsingleton.elim Lean.Meta.instFastSubsingletonForall Lean.Meta.instFastSubsingletonDecidable Fintype.instFastSubsingleton Matrix.ext Algebra.PreSubmersivePresentation.jacobiMatrix_apply Algebra.Presentation.map_relationOfHasCoeffs
map_jacobianRelationsOfHasCoeffs 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.map algebraMap jacobianRelationsOfHasCoeffs jacobianRelations	—	MvPolynomial.mem_range_map_iff_coeffs_subset HasSubset.Subset.trans Set.instIsTransSubset Set.subset_iUnion jacobian_isUnit Set.subset_union_right HasCoeffs.coeffs_subset_range
sum_jacobianRelationsOfHasCoeffs_mul_relationOfHasCoeffs 📖	mathematical	—	Finset.sum MvPolynomial CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MvPolynomial.instCommRingMvPolynomial Finset.univ Distrib.toMul NonUnitalNonAssocSemiring.toDistrib jacobianRelationsOfHasCoeffs Algebra.Presentation.relationOfHasCoeffs Algebra.PreSubmersivePresentation.toPresentation toPreSubmersivePresentation instHasCoeffs SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing jacobianOfHasCoeffs invJacobianOfHasCoeffs AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	MvPolynomial.map_injective FaithfulSMul.algebraMap_injective instHasCoeffs jacobian_isUnit map_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Finset.sum_congr map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_jacobianRelationsOfHasCoeffs Algebra.Presentation.map_relationOfHasCoeffs jacobianRelations_spec map_sub map_jacobianOfHasCoeffs map_invJacobianOfHasCoeffs map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass

Algebra.SubmersivePresentation.HasCoeffs

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeffs_subset_range 📖	mathematical	—	Set Set.instHasSubset Algebra.SubmersivePresentation.coeffs SetLike.coe Subring CommRing.toRing Subring.instSetLike RingHom.range algebraMap CommRing.toCommSemiring CommSemiring.toSemiring	—	—

---

← Back to Index