Lifts

📁 Source: Mathlib/Algebra/Polynomial/Lifts.lean

Statistics

Metric	Count
Definitions `Lifts`, `lifts`, `liftsRing`	3
Theorems `C'_mem_lifts`, `C_mem_lifts`, `X_mem_lifts`, `X_pow_mem_lifts`, `base_mul_mem_lifts`, `erase_mem_lifts`, `exists_degree_eq_of_mem_lifts`, `exists_support_eq_of_mem_lifts`, `lifts_and_degree_eq_and_monic`, `lifts_and_natDegree_eq_and_monic`, `lifts_iff_coeff_lifts`, `lifts_iff_coeffs_subset_range`, `lifts_iff_liftsRing`, `lifts_iff_ringHom_rangeS`, `lifts_iff_set_range`, `mem_lifts`, `mem_lifts_and_degree_eq`, `mem_lifts_iff_mem_alg`, `monic_of_monic_mapAlg`, `monomial_mem_lifts`, `monomial_mem_lifts_and_degree_eq`, `smul_mem_lifts`	22
Total	25

IntermediateField

Definitions

Name	Category	Theorems
`Lifts` 📖	CompData	10 math math: `Lifts.lt_iff_le_carrier_ne`, `Lifts.exists_lift_of_splits'`, `Lifts.eq_iff_le_carrier_eq`, `Lifts.le_union`, `Lifts.lt_iff`, `Lifts.exists_lift_of_splits`, `Lifts.carrier_union`, `Lifts.le_of_carrier_le_iSup`, `Lifts.exists_upper_bound`, `Lifts.le_iff`

Polynomial

Definitions

Name	Category	Theorems
`lifts` 📖	CompOp	22 math math: `mem_lifts_iff_mem_alg`, `IsPrimitive.map_mul_mem_lifts_iff`, `monomial_mem_lifts`, `X_mem_lifts`, `Splits.mem_lift_of_roots_mem_range`, `C_mem_lifts`, `mem_lifts`, `lifts_iff_ringHom_rangeS`, `IsPrimitive.mul_map_mem_lifts_iff`, `C'_mem_lifts`, `smul_mem_lifts`, `IsLocalization.scaleRoots_commonDenom_mem_lifts`, `lifts_iff_coeff_lifts`, `X_pow_mem_lifts`, `lifts_iff_liftsRing`, `lifts_iff_set_range`, `erase_mem_lifts`, `base_mul_mem_lifts`, `Algebra.IsInvariant.charpoly_mem_lifts`, `mem_lift_of_splits_of_roots_mem_range`, `integralClosure.mem_lifts_of_monic_of_dvd_map`, `lifts_iff_coeffs_subset_range`
`liftsRing` 📖	CompOp	1 math math: `lifts_iff_liftsRing`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`C'_mem_lifts` 📖	mathematical	`Set` `Set.instMembership` `Set.range` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	`Polynomial` `Subsemiring` `Semiring.toNonAssocSemiring` `semiring` `SetLike.instMembership` `Subsemiring.instSetLike` `lifts` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `C`	—	`Set.mem_range` `map_C`
`C_mem_lifts` 📖	mathematical	—	`Polynomial` `Subsemiring` `Semiring.toNonAssocSemiring` `semiring` `SetLike.instMembership` `Subsemiring.instSetLike` `lifts` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `C`	—	`map_C`
`X_mem_lifts` 📖	mathematical	—	`Polynomial` `Subsemiring` `Semiring.toNonAssocSemiring` `semiring` `SetLike.instMembership` `Subsemiring.instSetLike` `lifts` `X`	—	`map_X`
`X_pow_mem_lifts` 📖	mathematical	—	`Polynomial` `Subsemiring` `Semiring.toNonAssocSemiring` `semiring` `SetLike.instMembership` `Subsemiring.instSetLike` `lifts` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X`	—	`map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_X`
`base_mul_mem_lifts` 📖	mathematical	`Polynomial` `Subsemiring` `Semiring.toNonAssocSemiring` `semiring` `SetLike.instMembership` `Subsemiring.instSetLike` `lifts`	`Polynomial` `Subsemiring` `Semiring.toNonAssocSemiring` `semiring` `SetLike.instMembership` `Subsemiring.instSetLike` `lifts` `instMul` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `C`	—	`map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `map_C`
`erase_mem_lifts` 📖	mathematical	`Polynomial` `Subsemiring` `Semiring.toNonAssocSemiring` `semiring` `SetLike.instMembership` `Subsemiring.instSetLike` `lifts`	`Polynomial` `Subsemiring` `Semiring.toNonAssocSemiring` `semiring` `SetLike.instMembership` `Subsemiring.instSetLike` `lifts` `erase`	—	`lifts_iff_ringHom_rangeS` `mem_map_rangeS` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `erase_same` `erase_ne`
`exists_degree_eq_of_mem_lifts` 📖	mathematical	`Polynomial` `Subsemiring` `Semiring.toNonAssocSemiring` `semiring` `SetLike.instMembership` `Subsemiring.instSetLike` `lifts`	`Polynomial` `map` `degree`	—	`exists_support_eq_of_mem_lifts`
`exists_support_eq_of_mem_lifts` 📖	mathematical	`Polynomial` `Subsemiring` `Semiring.toNonAssocSemiring` `semiring` `SetLike.instMembership` `Subsemiring.instSetLike` `lifts`	`Polynomial` `map` `support`	—	`lifts_iff_coeff_lifts` `map_sum` `Finset.sum_congr` `map_monomial` `finset_sum_coeff` `coeff_monomial` `Finset.sum_ite_eq'` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`lifts_and_degree_eq_and_monic` 📖	mathematical	`Polynomial` `Subsemiring` `Semiring.toNonAssocSemiring` `semiring` `SetLike.instMembership` `Subsemiring.instSetLike` `lifts` `Monic`	`Polynomial` `map` `degree` `Monic`	—	`lifts_iff_coeff_lifts` `map_add` `map_sum` `Finset.sum_congr` `map_mul` `map_pow` `map_X` `map_C` `Monic.as_sum` `monic_X_pow_add` `Monic.degree_map`
`lifts_and_natDegree_eq_and_monic` 📖	mathematical	`Polynomial` `Subsemiring` `Semiring.toNonAssocSemiring` `semiring` `SetLike.instMembership` `Subsemiring.instSetLike` `lifts` `Monic`	`Polynomial` `map` `natDegree` `Monic`	—	`subsingleton_or_nontrivial` `Unique.instSubsingleton` `natDegree_one` `lifts_and_degree_eq_and_monic` `natDegree_eq_of_degree_eq`
`lifts_iff_coeff_lifts` 📖	mathematical	—	`Polynomial` `Subsemiring` `Semiring.toNonAssocSemiring` `semiring` `SetLike.instMembership` `Subsemiring.instSetLike` `lifts` `Set` `Set.instMembership` `Set.range` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `coeff`	—	`lifts_iff_ringHom_rangeS` `mem_map_rangeS`
`lifts_iff_coeffs_subset_range` 📖	mathematical	—	`Polynomial` `Subsemiring` `Semiring.toNonAssocSemiring` `semiring` `SetLike.instMembership` `Subsemiring.instSetLike` `lifts` `Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `coeffs` `Set.range` `DFunLike.coe` `RingHom` `RingHom.instFunLike`	—	`lifts_iff_coeff_lifts` `mem_coeffs_iff` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `coeff_mem_coeffs`
`lifts_iff_liftsRing` 📖	mathematical	—	`Polynomial` `Ring.toSemiring` `Subsemiring` `Semiring.toNonAssocSemiring` `semiring` `SetLike.instMembership` `Subsemiring.instSetLike` `lifts` `Subring` `Ring.toNonAssocRing` `ring` `Subring.instSetLike` `liftsRing`	—	—
`lifts_iff_ringHom_rangeS` 📖	mathematical	—	`Polynomial` `Subsemiring` `Semiring.toNonAssocSemiring` `semiring` `SetLike.instMembership` `Subsemiring.instSetLike` `lifts` `RingHom.rangeS` `mapRingHom`	—	—
`lifts_iff_set_range` 📖	mathematical	—	`Polynomial` `Subsemiring` `Semiring.toNonAssocSemiring` `semiring` `SetLike.instMembership` `Subsemiring.instSetLike` `lifts` `Set` `Set.instMembership` `Set.range` `map`	—	—
`mem_lifts` 📖	mathematical	—	`Polynomial` `Subsemiring` `Semiring.toNonAssocSemiring` `semiring` `SetLike.instMembership` `Subsemiring.instSetLike` `lifts` `map`	—	—
`mem_lifts_and_degree_eq` 📖	mathematical	`Polynomial` `Subsemiring` `Semiring.toNonAssocSemiring` `semiring` `SetLike.instMembership` `Subsemiring.instSetLike` `lifts`	`Polynomial` `map` `degree`	—	`exists_degree_eq_of_mem_lifts`
`mem_lifts_iff_mem_alg` 📖	mathematical	—	`Polynomial` `Subsemiring` `Semiring.toNonAssocSemiring` `semiring` `SetLike.instMembership` `Subsemiring.instSetLike` `lifts` `CommSemiring.toSemiring` `algebraMap` `Subalgebra` `algebraOfAlgebra` `Subalgebra.instSetLike` `AlgHom.range` `Algebra.id` `mapAlg`	—	`mapAlg_eq_map`
`monic_of_monic_mapAlg` 📖	mathematical	`Monic` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `mapAlg`	`Monic` `CommSemiring.toSemiring`	—	`monic_of_injective` `FaithfulSMul.algebraMap_injective`
`monomial_mem_lifts` 📖	mathematical	`Set` `Set.instMembership` `Set.range` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	`Polynomial` `Subsemiring` `Semiring.toNonAssocSemiring` `semiring` `SetLike.instMembership` `Subsemiring.instSetLike` `lifts` `DFunLike.coe` `LinearMap` `RingHom.id` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial`	—	`Set.mem_range` `map_monomial`
`monomial_mem_lifts_and_degree_eq` 📖	mathematical	`Polynomial` `Subsemiring` `Semiring.toNonAssocSemiring` `semiring` `SetLike.instMembership` `Subsemiring.instSetLike` `lifts` `DFunLike.coe` `LinearMap` `RingHom.id` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial`	`Polynomial` `map` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial` `degree`	—	`eq_or_ne` `map_zero` `monomial_zero_right` `lifts_iff_coeff_lifts` `coeff_monomial_same` `map_monomial` `degree_monomial` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`smul_mem_lifts` 📖	mathematical	`Polynomial` `Subsemiring` `Semiring.toNonAssocSemiring` `semiring` `SetLike.instMembership` `Subsemiring.instSetLike` `lifts` `CommSemiring.toSemiring` `algebraMap`	`Polynomial` `Subsemiring` `Semiring.toNonAssocSemiring` `semiring` `SetLike.instMembership` `Subsemiring.instSetLike` `lifts` `CommSemiring.toSemiring` `algebraMap` `Algebra.toSMul` `algebraOfAlgebra`	—	`mem_lifts_iff_mem_alg` `Subalgebra.smul_mem`

---

← Back to Index