Documentation Verification Report

StandardEtale

📁 Source: Mathlib/RingTheory/Etale/StandardEtale.lean

Statistics

Metric	Count
Definitions `IsStandardEtale`, `StandardEtalePair`, `HasMap`, `X`, `equivAwayAdjoinRoot`, `equivAwayQuotient`, `equivMvPolynomialQuotient`, `equivPolynomialQuotient`, `f`, `g`, `homEquiv`, `instAlgebraRing`, `instCommRingRing`, `map`, `StandardEtalePresentation`, `P`, `baseChange`, `equivRing`, `mapEquiv`, `toPresentation`, `toSubmersivePresentation`, `x`	22
Theorems `nonempty_standardEtalePresentation`, `of_equiv`, `of_isLocalizationAway`, `of_surjective`, `instEtaleOfIsStandardEtale`, `instIsStandardEtale`, `instIsStandardEtaleRing`, `instIsStandardEtaleTensorProduct`, `isUnit_derivative_f`, `map`, `map_algebraMap`, `aeval_X_g_mul_mk_X`, `cond`, `equivMvPolynomialQuotient_symm_apply`, `existsUnique_hasMap_of_hasMap_quotient_of_sq_eq_bot`, `hasMap_X`, `homEquiv_apply_coe`, `homEquiv_symm_apply`, `hom_ext`, `hom_ext_iff`, `instEtaleRing`, `instFormallyEtaleRing`, `inv_aeval_X_g`, `lift_X`, `lift_X_left`, `map_f`, `map_g`, `monic_f`, `aeval_val_equivMvPolynomial`, `equivRing_symm_X`, `equivRing_x`, `exists_mul_aeval_x_g_pow_eq_aeval_x`, `hasMap`, `hom_ext`, `lift_bijective`, `toPresentation_algebra_algebraMap_apply`, `toPresentation_algebra_smul`, `toPresentation_relation`, `toPresentation_val`, `toPresentation_σ'`, `toSubmersivePresentation_jacobian`, `toSubmersivePresentation_map`, `toSubmersivePresentation_toPreSubmersivePresentation_toPresentation`	43
Total	65

Algebra

Definitions

Name	Category	Theorems
`IsStandardEtale` 📖	CompData	9 math math: `HasStandardEtaleSurjectionOn.isStandardEtale`, `instIsStandardEtaleRing`, `IsSmoothAt.exists_isStandardEtale_mvPolynomial`, `IsStandardEtale.of_equiv`, `IsEtaleAt.exists_isStandardEtale`, `IsStandardEtale.of_surjective`, `instIsStandardEtale`, `IsStandardEtale.of_isLocalizationAway`, `instIsStandardEtaleTensorProduct`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instEtaleOfIsStandardEtale` 📖	mathematical	—	`Etale`	—	`Etale.of_equiv` `IsStandardEtale.nonempty_standardEtalePresentation` `StandardEtalePair.instEtaleRing`
`instIsStandardEtale` 📖	mathematical	—	`IsStandardEtale` `id` `CommRing.toCommSemiring`	—	`Polynomial.derivative_X` `mul_one` `MulZeroClass.mul_zero` `add_zero` `pow_zero` `Polynomial.aeval_X` `Polynomial.eval_one` `Ideal.Quotient.eq_zero_iff_mem` `Ideal.subset_span` `Set.mem_insert` `ext_id` `StandardEtalePair.hom_ext` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `RingHom.instRingHomClass` `AlgEquiv.bijective`
`instIsStandardEtaleRing` 📖	mathematical	—	`IsStandardEtale` `StandardEtalePair.Ring` `StandardEtalePair.instCommRingRing` `StandardEtalePair.instAlgebraRing`	—	`StandardEtalePair.hasMap_X` `StandardEtalePair.lift_X_left` `Function.bijective_id`
`instIsStandardEtaleTensorProduct` 📖	mathematical	—	`IsStandardEtale` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `toModule` `CommSemiring.toSemiring` `TensorProduct.instCommRing` `TensorProduct.leftAlgebra` `id` `to_smulCommClass`	—	`to_smulCommClass` `IsStandardEtale.nonempty_standardEtalePresentation`

Algebra.IsStandardEtale

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nonempty_standardEtalePresentation` 📖	mathematical	—	`StandardEtalePresentation`	—	—
`of_equiv` 📖	mathematical	—	`Algebra.IsStandardEtale`	—	`nonempty_standardEtalePresentation`
`of_isLocalizationAway` 📖	mathematical	—	`Algebra.IsStandardEtale`	—	`nonempty_standardEtalePresentation` `StandardEtalePresentation.exists_mul_aeval_x_g_pow_eq_aeval_x` `StandardEtalePair.monic_f` `StandardEtalePair.cond` `Mathlib.Tactic.LinearCombination.eq_of_eq` `AddRightCancelSemigroup.toIsRightCancelAdd` `Mathlib.Tactic.LinearCombination.mul_eq_const` `Mathlib.Tactic.LinearCombination.eq_rearrange` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `IsLocalization.Away.mul` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `Localization.isLocalization` `MonoidHom.instMonoidHomClass` `Polynomial.algHom_ext` `IsLocalization.lift_eq` `AdjoinRoot.lift_root` `StandardEtalePresentation.equivRing_symm_X` `Polynomial.aeval_X` `Submonoid.map_powers` `IsLocalization.Away.of_associated` `IsUnit.pow` `StandardEtalePresentation.hasMap` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `RingEquiv.map_mul'` `RingEquiv.map_add'` `AlgEquivClass.toRingEquivClass` `AlgEquiv.instAlgEquivClass` `IsScalarTower.algebraMap_apply` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `IsLocalization.map_eq` `AlgEquiv.commutes` `IsScalarTower.algebraMap_eq` `of_equiv` `Algebra.instIsStandardEtaleRing`
`of_surjective` 📖	mathematical	`DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AlgHom.funLike`	`Algebra.IsStandardEtale`	—	`IsScalarTower.of_algebraMap_eq'` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.comp_algebraMap` `RingHom.instRingHomClass` `IsScalarTower.right` `Ideal.isIdempotentElem_iff_of_fg` `Algebra.FinitePresentation.ker_fG_of_surjective` `Algebra.Etale.finitePresentation` `Algebra.instEtaleOfIsStandardEtale` `Algebra.FormallyEtale.iff_of_surjective` `Algebra.FormallyEtale.of_restrictScalars` `Algebra.FormallyEtale.instFormallyUnramified` `Algebra.Etale.formallyEtale` `IsLocalization.away_of_isIdempotentElem` `IsIdempotentElem.one_sub` `sub_sub_cancel` `of_isLocalizationAway`

StandardEtalePair

Definitions

Name	Category	Theorems
`HasMap` 📖	MathDef	4 math math: `homEquiv_symm_apply`, `StandardEtalePresentation.hasMap`, `homEquiv_apply_coe`, `hasMap_X`
`X` 📖	CompOp	10 math math: `inv_aeval_X_g`, `homEquiv_apply_coe`, `hasMap_X`, `equivMvPolynomialQuotient_symm_apply`, `lift_X`, `StandardEtalePresentation.equivRing_x`, `hom_ext_iff`, `aeval_X_g_mul_mk_X`, `lift_X_left`, `StandardEtalePresentation.equivRing_symm_X`
`equivAwayAdjoinRoot` 📖	CompOp	—
`equivAwayQuotient` 📖	CompOp	—
`equivMvPolynomialQuotient` 📖	CompOp	6 math math: `StandardEtalePresentation.toPresentation_algebra_smul`, `equivMvPolynomialQuotient_symm_apply`, `StandardEtalePresentation.toPresentation_σ'`, `StandardEtalePresentation.toPresentation_algebra_algebraMap_apply`, `StandardEtalePresentation.toPresentation_val`, `StandardEtalePresentation.toPresentation_relation`
`equivPolynomialQuotient` 📖	CompOp	—
`f` 📖	CompOp	13 math math: `inv_aeval_X_g`, `StandardEtalePresentation.toPresentation_algebra_smul`, `equivMvPolynomialQuotient_symm_apply`, `monic_f`, `map_f`, `StandardEtalePresentation.toSubmersivePresentation_jacobian`, `StandardEtalePresentation.toPresentation_σ'`, `HasMap.isUnit_derivative_f`, `cond`, `aeval_X_g_mul_mk_X`, `StandardEtalePresentation.toPresentation_algebra_algebraMap_apply`, `StandardEtalePresentation.toPresentation_val`, `StandardEtalePresentation.toPresentation_relation`
`g` 📖	CompOp	12 math math: `inv_aeval_X_g`, `StandardEtalePresentation.toPresentation_algebra_smul`, `equivMvPolynomialQuotient_symm_apply`, `map_g`, `StandardEtalePresentation.toSubmersivePresentation_jacobian`, `StandardEtalePresentation.exists_mul_aeval_x_g_pow_eq_aeval_x`, `StandardEtalePresentation.toPresentation_σ'`, `cond`, `aeval_X_g_mul_mk_X`, `StandardEtalePresentation.toPresentation_algebra_algebraMap_apply`, `StandardEtalePresentation.toPresentation_val`, `StandardEtalePresentation.toPresentation_relation`
`homEquiv` 📖	CompOp	2 math math: `homEquiv_symm_apply`, `homEquiv_apply_coe`
`instAlgebraRing` 📖	CompOp	20 math math: `inv_aeval_X_g`, `Algebra.instIsStandardEtaleRing`, `homEquiv_symm_apply`, `StandardEtalePresentation.toPresentation_algebra_smul`, `homEquiv_apply_coe`, `hasMap_X`, `equivMvPolynomialQuotient_symm_apply`, `instFormallyEtaleRing`, `lift_X`, `StandardEtalePresentation.equivRing_x`, `StandardEtalePresentation.lift_bijective`, `hom_ext_iff`, `StandardEtalePresentation.toPresentation_σ'`, `aeval_X_g_mul_mk_X`, `StandardEtalePresentation.toPresentation_algebra_algebraMap_apply`, `StandardEtalePresentation.toPresentation_val`, `lift_X_left`, `StandardEtalePresentation.toPresentation_relation`, `instEtaleRing`, `StandardEtalePresentation.equivRing_symm_X`
`instCommRingRing` 📖	CompOp	20 math math: `inv_aeval_X_g`, `Algebra.instIsStandardEtaleRing`, `homEquiv_symm_apply`, `StandardEtalePresentation.toPresentation_algebra_smul`, `homEquiv_apply_coe`, `hasMap_X`, `equivMvPolynomialQuotient_symm_apply`, `instFormallyEtaleRing`, `lift_X`, `StandardEtalePresentation.equivRing_x`, `StandardEtalePresentation.lift_bijective`, `hom_ext_iff`, `StandardEtalePresentation.toPresentation_σ'`, `aeval_X_g_mul_mk_X`, `StandardEtalePresentation.toPresentation_algebra_algebraMap_apply`, `StandardEtalePresentation.toPresentation_val`, `lift_X_left`, `StandardEtalePresentation.toPresentation_relation`, `instEtaleRing`, `StandardEtalePresentation.equivRing_symm_X`
`map` 📖	CompOp	3 math math: `map_g`, `map_f`, `HasMap.map_algebraMap`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aeval_X_g_mul_mk_X` 📖	mathematical	—	`Ring` `HasQuotient.Quotient` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.semiring` `Ideal` `Ring.toSemiring` `Polynomial.ring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.span` `Set` `Set.instInsert` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C` `f` `Set.instSingletonSet` `Polynomial.instSub` `Polynomial.instMul` `Polynomial.X` `g` `Polynomial.instOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRingRing` `AlgHom` `Polynomial.algebraOfAlgebra` `Algebra.id` `instAlgebraRing` `AlgHom.funLike` `Polynomial.aeval` `X` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `Polynomial.commRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`Ideal.instIsTwoSided_1` `Polynomial.algHom_ext` `Polynomial.aeval_X` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `sub_eq_zero` `map_sub` `RingHomClass.toAddMonoidHomClass` `mul_comm` `Ideal.Quotient.eq_zero_iff_mem` `Ideal.subset_span` `Set.mem_insert_of_mem`
`cond` 📖	mathematical	—	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.instAdd` `Polynomial.instMul` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.semiring` `Polynomial.module` `Semiring.toModule` `LinearMap.instFunLike` `Polynomial.derivative` `f` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `g`	—	—
`equivMvPolynomialQuotient_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `HasQuotient.Quotient` `MvPolynomial` `CommRing.toCommSemiring` `Ideal` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `Ideal.instHasQuotient_1` `MvPolynomial.instCommRingMvPolynomial` `Ideal.span` `Set` `Set.instInsert` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `MvPolynomial.algebra` `AlgEquiv.instFunLike` `Polynomial.Bivariate.equivMvPolynomial` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C` `f` `Set.instSingletonSet` `Polynomial.instSub` `Polynomial.ring` `CommRing.toRing` `Polynomial.instMul` `Polynomial.X` `g` `Polynomial.instOne` `Ring` `Ideal.Quotient.semiring` `instCommRingRing` `Ideal.instAlgebraQuotient` `instAlgebraRing` `AlgEquiv.symm` `equivMvPolynomialQuotient` `Ring.toSemiring` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `MvPolynomial.X` `X`	—	`Ideal.instIsTwoSided_1` `Polynomial.Bivariate.equivMvPolynomial_symm_X_0`
`existsUnique_hasMap_of_hasMap_quotient_of_sq_eq_bot` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id` `Bot.bot` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `HasMap` `HasQuotient.Quotient` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.commRing` `Ideal.instAlgebraQuotient` `DFunLike.coe` `RingHom` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike`	`ExistsUnique` `SetLike.instMembership` `Submodule.setLike` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Ideal.instIsTwoSided_1` `Ideal.Quotient.eq_zero_iff_mem` `Polynomial.aeval_algHom_apply` `AlgHom.algHomClass` `Ideal.Quotient.mk_surjective` `cond` `Mathlib.Tactic.LinearCombination.eq_of_eq` `AddRightCancelSemigroup.toIsRightCancelAdd` `Mathlib.Tactic.LinearCombination.mul_const_eq` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `Mathlib.Tactic.LinearCombination.eq_rearrange` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `sub_mem` `Submodule.addSubgroupClass` `Ideal.mem_of_dvd` `sub_one_dvd_pow_sub_one` `map_one` `MonoidHomClass.toOneHomClass` `Ideal.mul_mem_right` `sub_eq_iff_eq_add'` `Eq.le` `Ideal.pow_mem_pow` `pow_two` `Ideal.mul_mem_mul` `Polynomial.aeval_add_of_sq_eq_zero` `IsNilpotent.isUnit_quotient_mk_iff` `IsScalarTower.right` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `add_zero`
`hasMap_X` 📖	mathematical	—	`HasMap` `Ring` `instCommRingRing` `instAlgebraRing` `X`	—	`Ideal.instIsTwoSided_1` `Polynomial.algHom_ext` `Polynomial.aeval_X` `Ideal.Quotient.eq_zero_iff_mem` `Ideal.subset_span` `Set.mem_insert` `IsUnit.of_mul_eq_one` `instIsDedekindFiniteMonoid` `aeval_X_g_mul_mk_X`
`homEquiv_apply_coe` 📖	mathematical	—	`HasMap` `DFunLike.coe` `Equiv` `AlgHom` `Ring` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `instCommRingRing` `instAlgebraRing` `EquivLike.toFunLike` `Equiv.instEquivLike` `homEquiv` `AlgHom.funLike` `X`	—	—
`homEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `HasMap` `AlgHom` `Ring` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `instCommRingRing` `instAlgebraRing` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `homEquiv` `lift`	—	—
`hom_ext` 📖	—	`DFunLike.coe` `AlgHom` `Ring` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `instCommRingRing` `instAlgebraRing` `AlgHom.funLike` `X`	—	—	`Ideal.instIsTwoSided_1` `Polynomial.algHom_ext` `Polynomial.aeval_X` `Ideal.Quotient.algHom_ext` `Polynomial.algHom_ext'` `hasMap_X` `Units.mul_eq_one_iff_inv_eq` `aeval_X_g_mul_mk_X` `Units.coe_map_inv` `Units.ext` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `IsUnit.unit.congr_simp`
`hom_ext_iff` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Ring` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `instCommRingRing` `instAlgebraRing` `AlgHom.funLike` `X`	—	`hom_ext`
`instEtaleRing` 📖	mathematical	—	`Algebra.Etale` `Ring` `instCommRingRing` `instAlgebraRing`	—	`instFormallyEtaleRing` `Algebra.FinitePresentation.quotient` `Submodule.fg_span` `Polynomial.X_mul_C` `Algebra.FinitePresentation.polynomial` `Algebra.FinitePresentation.self`
`instFormallyEtaleRing` 📖	mathematical	—	`Algebra.FormallyEtale` `Ring` `instCommRingRing` `instAlgebraRing`	—	`Ideal.instIsTwoSided_1` `Algebra.FormallyEtale.iff_comp_bijective` `Function.Bijective.of_comp_iff` `Equiv.bijective` `Function.Bijective.of_comp_iff'` `existsUnique_hasMap_of_hasMap_quotient_of_sq_eq_bot` `add_sub_cancel_left` `sub_eq_iff_eq_add'` `add_sub_cancel` `lift_X` `Function.Surjective.forall` `Ideal.Quotient.mk_surjective`
`inv_aeval_X_g` 📖	mathematical	—	`Units.val` `Ring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRingRing` `Units` `Units.instInv` `IsUnit.unit` `DFunLike.coe` `AlgHom` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `instAlgebraRing` `AlgHom.funLike` `Polynomial.aeval` `X` `g` `f` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `IsUnit` `hasMap_X` `RingHom` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `Polynomial.ring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.span` `Set` `Set.instInsert` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C` `Set.instSingletonSet` `Polynomial.instSub` `Polynomial.instMul` `Polynomial.X` `Polynomial.instOne` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `Polynomial.commRing`	—	`hasMap_X` `Ideal.instIsTwoSided_1` `Units.mul_eq_one_iff_inv_eq` `aeval_X_g_mul_mk_X`
`lift_X` 📖	mathematical	`HasMap`	`DFunLike.coe` `AlgHom` `Ring` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `instCommRingRing` `instAlgebraRing` `AlgHom.funLike` `lift` `X`	—	`Polynomial.aeval_C` `Polynomial.map_X` `Polynomial.eval_X`
`lift_X_left` 📖	mathematical	—	`lift` `Ring` `instCommRingRing` `instAlgebraRing` `X` `hasMap_X` `AlgHom.id` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	—	`hom_ext` `hasMap_X` `lift_X`
`map_f` 📖	mathematical	—	`f` `map` `Polynomial.map` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	—
`map_g` 📖	mathematical	—	`g` `map` `Polynomial.map` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	—
`monic_f` 📖	mathematical	—	`Polynomial.Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `f`	—	—

StandardEtalePair.HasMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isUnit_derivative_f` 📖	mathematical	`StandardEtalePair.HasMap`	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.module` `Semiring.toModule` `LinearMap.instFunLike` `Polynomial.derivative` `StandardEtalePair.f`	—	`StandardEtalePair.cond` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `MulZeroClass.zero_mul` `add_zero` `isUnit_of_dvd_unit` `IsUnit.pow`
`map` 📖	mathematical	`StandardEtalePair.HasMap`	`DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AlgHom.funLike`	—	`Polynomial.aeval_algHom` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `IsUnit.map` `MonoidWithZeroHomClass.toMonoidHomClass`
`map_algebraMap` 📖	mathematical	`StandardEtalePair.HasMap`	`StandardEtalePair.map` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	—	`Polynomial.aeval_map_algebraMap`

StandardEtalePresentation

Definitions

Name	Category	Theorems
`P` 📖	CompOp	11 math math: `toPresentation_algebra_smul`, `hasMap`, `equivRing_x`, `toSubmersivePresentation_jacobian`, `exists_mul_aeval_x_g_pow_eq_aeval_x`, `lift_bijective`, `toPresentation_σ'`, `toPresentation_algebra_algebraMap_apply`, `toPresentation_val`, `toPresentation_relation`, `equivRing_symm_X`
`baseChange` 📖	CompOp	—
`equivRing` 📖	CompOp	2 math math: `equivRing_x`, `equivRing_symm_X`
`mapEquiv` 📖	CompOp	—
`toPresentation` 📖	CompOp	7 math math: `toPresentation_algebra_smul`, `toSubmersivePresentation_toPreSubmersivePresentation_toPresentation`, `toPresentation_σ'`, `aeval_val_equivMvPolynomial`, `toPresentation_algebra_algebraMap_apply`, `toPresentation_val`, `toPresentation_relation`
`toSubmersivePresentation` 📖	CompOp	3 math math: `toSubmersivePresentation_toPreSubmersivePresentation_toPresentation`, `toSubmersivePresentation_map`, `toSubmersivePresentation_jacobian`
`x` 📖	CompOp	12 math math: `toPresentation_algebra_smul`, `hasMap`, `equivRing_x`, `toSubmersivePresentation_jacobian`, `exists_mul_aeval_x_g_pow_eq_aeval_x`, `lift_bijective`, `toPresentation_σ'`, `aeval_val_equivMvPolynomial`, `toPresentation_algebra_algebraMap_apply`, `toPresentation_val`, `toPresentation_relation`, `equivRing_symm_X`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aeval_val_equivMvPolynomial` 📖	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` `toPresentation` `AlgEquiv` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `AlgEquiv.instFunLike` `Polynomial.Bivariate.equivMvPolynomial` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C` `Polynomial.aeval` `x`	—	`Polynomial.algHom_ext` `Polynomial.Bivariate.equivMvPolynomial_C_X` `MvPolynomial.aeval_X` `hasMap` `StandardEtalePair.equivMvPolynomialQuotient_symm_apply` `StandardEtalePair.lift_X` `Polynomial.aeval_X`
`equivRing_symm_X` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `StandardEtalePair.Ring` `P` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `StandardEtalePair.instCommRingRing` `StandardEtalePair.instAlgebraRing` `AlgEquiv.instFunLike` `AlgEquiv.symm` `equivRing` `StandardEtalePair.X` `x`	—	`StandardEtalePair.lift_X` `hasMap`
`equivRing_x` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `StandardEtalePair.Ring` `P` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `StandardEtalePair.instCommRingRing` `StandardEtalePair.instAlgebraRing` `AlgEquiv.instFunLike` `equivRing` `x` `StandardEtalePair.X`	—	`AlgEquiv.symm_apply_eq` `equivRing_symm_X`
`exists_mul_aeval_x_g_pow_eq_aeval_x` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `x` `StandardEtalePair.g` `P`	—	`AlgEquiv.surjective` `IsLocalization.surj` `Localization.isLocalization` `AdjoinRoot.mk_surjective` `AlgEquiv.injective` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `AlgEquiv.apply_symm_apply` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `equivRing_x` `RingHom.instRingHomClass` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `IsLocalization.lift_eq`
`hasMap` 📖	mathematical	—	`StandardEtalePair.HasMap` `P` `x`	—	—
`hom_ext` 📖	—	`DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `AlgHom.funLike` `x`	—	—	`StandardEtalePair.hom_ext` `equivRing_symm_X` `AlgHom.ext` `AlgEquiv.surjective`
`lift_bijective` 📖	mathematical	—	`Function.Bijective` `StandardEtalePair.Ring` `P` `DFunLike.coe` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `StandardEtalePair.instCommRingRing` `StandardEtalePair.instAlgebraRing` `AlgHom.funLike` `StandardEtalePair.lift` `x` `hasMap`	—	—
`toPresentation_algebra_algebraMap_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `CommRing.toCommSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `Algebra.algebraMap` `Algebra.Generators.algebra` `Algebra.Presentation.toGenerators` `toPresentation` `MvPolynomial.eval₂` `algebraMap` `StandardEtalePair.Ring` `P` `AlgHom` `StandardEtalePair.instCommRingRing` `StandardEtalePair.instAlgebraRing` `AlgHom.funLike` `StandardEtalePair.lift` `x` `hasMap` `HasQuotient.Quotient` `Ideal` `Ideal.instHasQuotient_1` `MvPolynomial.instCommRingMvPolynomial` `Ideal.span` `Set` `Set.instInsert` `AlgEquiv` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `MvPolynomial.algebra` `AlgEquiv.instFunLike` `Polynomial.Bivariate.equivMvPolynomial` `Polynomial.C` `StandardEtalePair.f` `Set.instSingletonSet` `Polynomial.instSub` `Polynomial.ring` `CommRing.toRing` `Polynomial.instMul` `Polynomial.X` `StandardEtalePair.g` `Polynomial.instOne` `Ideal.Quotient.semiring` `Ideal.instAlgebraQuotient` `AlgEquiv.symm` `StandardEtalePair.equivMvPolynomialQuotient` `Ring.toSemiring` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `MvPolynomial.X`	—	—
`toPresentation_algebra_smul` 📖	mathematical	—	`MvPolynomial` `CommRing.toCommSemiring` `Algebra.toSMul` `MvPolynomial.commSemiring` `CommSemiring.toSemiring` `Algebra.Generators.algebra` `Algebra.Presentation.toGenerators` `toPresentation` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `AlgHom` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike` `MvPolynomial.aeval` `StandardEtalePair.Ring` `P` `StandardEtalePair.instCommRingRing` `StandardEtalePair.instAlgebraRing` `StandardEtalePair.lift` `x` `hasMap` `HasQuotient.Quotient` `Ideal` `Ideal.instHasQuotient_1` `MvPolynomial.instCommRingMvPolynomial` `Ideal.span` `Set` `Set.instInsert` `AlgEquiv` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `AlgEquiv.instFunLike` `Polynomial.Bivariate.equivMvPolynomial` `RingHom` `RingHom.instFunLike` `Polynomial.C` `StandardEtalePair.f` `Set.instSingletonSet` `Polynomial.instSub` `Polynomial.ring` `CommRing.toRing` `Polynomial.instMul` `Polynomial.X` `StandardEtalePair.g` `Polynomial.instOne` `Ideal.Quotient.semiring` `Ideal.instAlgebraQuotient` `AlgEquiv.symm` `StandardEtalePair.equivMvPolynomialQuotient` `Ring.toSemiring` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `MvPolynomial.X`	—	—
`toPresentation_relation` 📖	mathematical	—	`Algebra.Presentation.relation` `toPresentation` `Matrix.vecCons` `Algebra.Generators.Ring` `Algebra.Generators.ofAlgHom` `AlgHom.comp` `MvPolynomial` `CommRing.toCommSemiring` `StandardEtalePair.Ring` `P` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `StandardEtalePair.instCommRingRing` `MvPolynomial.algebra` `Algebra.id` `StandardEtalePair.instAlgebraRing` `StandardEtalePair.lift` `x` `hasMap` `HasQuotient.Quotient` `Ideal` `Ideal.instHasQuotient_1` `MvPolynomial.instCommRingMvPolynomial` `Ideal.span` `Set` `Set.instInsert` `DFunLike.coe` `AlgEquiv` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `AlgEquiv.instFunLike` `Polynomial.Bivariate.equivMvPolynomial` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C` `StandardEtalePair.f` `Set.instSingletonSet` `Polynomial.instSub` `Polynomial.ring` `CommRing.toRing` `Polynomial.instMul` `Polynomial.X` `StandardEtalePair.g` `Polynomial.instOne` `Ideal.Quotient.semiring` `Ideal.instAlgebraQuotient` `AlgHomClass.toAlgHom` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instEquivLike` `AlgEquiv.instAlgEquivClass` `AlgEquiv.symm` `StandardEtalePair.equivMvPolynomialQuotient` `Ideal.Quotient.mkₐ` `SubNegMonoid.toSub` `SubtractionMonoid.toSubNegMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MvPolynomial.X` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Matrix.vecEmpty`	—	`hasMap` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `Polynomial.X_mul_C` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `Polynomial.Bivariate.equivMvPolynomial_X` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass`
`toPresentation_val` 📖	mathematical	—	`Algebra.Generators.val` `Algebra.Presentation.toGenerators` `toPresentation` `DFunLike.coe` `AlgHom` `StandardEtalePair.Ring` `P` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `StandardEtalePair.instCommRingRing` `StandardEtalePair.instAlgebraRing` `AlgHom.funLike` `StandardEtalePair.lift` `x` `hasMap` `AlgEquiv` `HasQuotient.Quotient` `MvPolynomial` `Ideal` `MvPolynomial.commSemiring` `Ideal.instHasQuotient_1` `MvPolynomial.instCommRingMvPolynomial` `Ideal.span` `Set` `Set.instInsert` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `MvPolynomial.algebra` `AlgEquiv.instFunLike` `Polynomial.Bivariate.equivMvPolynomial` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C` `StandardEtalePair.f` `Set.instSingletonSet` `Polynomial.instSub` `Polynomial.ring` `CommRing.toRing` `Polynomial.instMul` `Polynomial.X` `StandardEtalePair.g` `Polynomial.instOne` `Ideal.Quotient.semiring` `Ideal.instAlgebraQuotient` `AlgEquiv.symm` `StandardEtalePair.equivMvPolynomialQuotient` `Ring.toSemiring` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `MvPolynomial.X`	—	—
`toPresentation_σ'` 📖	mathematical	—	`Algebra.Generators.σ'` `Algebra.Presentation.toGenerators` `toPresentation` `MvPolynomial` `CommRing.toCommSemiring` `DFunLike.coe` `AlgHom` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike` `MvPolynomial.aeval` `StandardEtalePair.Ring` `P` `StandardEtalePair.instCommRingRing` `StandardEtalePair.instAlgebraRing` `StandardEtalePair.lift` `x` `hasMap` `HasQuotient.Quotient` `Ideal` `Ideal.instHasQuotient_1` `MvPolynomial.instCommRingMvPolynomial` `Ideal.span` `Set` `Set.instInsert` `AlgEquiv` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `AlgEquiv.instFunLike` `Polynomial.Bivariate.equivMvPolynomial` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C` `StandardEtalePair.f` `Set.instSingletonSet` `Polynomial.instSub` `Polynomial.ring` `CommRing.toRing` `Polynomial.instMul` `Polynomial.X` `StandardEtalePair.g` `Polynomial.instOne` `Ideal.Quotient.semiring` `Ideal.instAlgebraQuotient` `AlgEquiv.symm` `StandardEtalePair.equivMvPolynomialQuotient` `Ring.toSemiring` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `MvPolynomial.X` `AlgHom.comp` `AlgEquiv.toAlgHom` `Ideal.Quotient.mkₐ`	—	—
`toSubmersivePresentation_jacobian` 📖	mathematical	—	`Algebra.PreSubmersivePresentation.jacobian` `Algebra.SubmersivePresentation.toPreSubmersivePresentation` `Finite.of_fintype` `Fin.fintype` `toSubmersivePresentation` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `x` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.module` `Semiring.toModule` `LinearMap.instFunLike` `Polynomial.derivative` `StandardEtalePair.f` `P` `StandardEtalePair.g`	—	`Finite.of_fintype` `Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det` `Matrix.det_fin_two` `Algebra.PreSubmersivePresentation.jacobiMatrix_apply` `RingHomInvPair.ids` `toPresentation_relation` `Polynomial.Bivariate.pderiv_zero_equivMvPolynomial` `Derivation.mapCoeffs_C` `hasMap` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `Matrix.cons_val_fin_one` `map_sub` `Derivation.instAddMonoidHomClass` `Derivation.leibniz` `MvPolynomial.pderiv_X` `Pi.single_eq_same` `mul_one` `Polynomial.Bivariate.pderiv_one_equivMvPolynomial` `Polynomial.derivative_C` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `MulZeroClass.mul_zero` `add_zero` `Derivation.map_one_eq_zero` `sub_zero` `Pi.single_eq_of_ne` `Fin.instNeZeroHAddNatOfNat_mathlib_1` `zero_add` `Algebra.Generators.algebraMap_apply` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `aeval_val_equivMvPolynomial`
`toSubmersivePresentation_map` 📖	mathematical	—	`Algebra.PreSubmersivePresentation.map` `Algebra.SubmersivePresentation.toPreSubmersivePresentation` `Finite.of_fintype` `Fin.fintype` `toSubmersivePresentation`	—	`Finite.of_fintype`
`toSubmersivePresentation_toPreSubmersivePresentation_toPresentation` 📖	mathematical	—	`Algebra.PreSubmersivePresentation.toPresentation` `Algebra.SubmersivePresentation.toPreSubmersivePresentation` `Finite.of_fintype` `Fin.fintype` `toSubmersivePresentation` `toPresentation`	—	`Finite.of_fintype`

(root)

Definitions

Name	Category	Theorems
`StandardEtalePair` 📖	CompData	—
`StandardEtalePresentation` 📖	CompData	1 math math: `Algebra.IsStandardEtale.nonempty_standardEtalePresentation`

---

← Back to Index