GeometricallyReduced_isReduced_tensorProduct_of_separablyGenerated.lean`

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)

Mathlib

class IsSeparablyGenerated line 40 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra
4 instances, coercions and auxiliary constants left out.
Also declared: APNOutputs/StacksProject/GeometricallyReduced_isGeometricallyReduced_iff_of_separable_algebraic.lean:40 (same declaration text), APNOutputs/StacksProject/GeometricallyReduced_isReduced_tensorProduct_of_separable.lean:40 (same declaration text), APNOutputs/StacksProject/Separability_exists_isPurelyInseparable_isSeparablyGenerated_of_essFiniteType.lean:40 (same declaration text).
class IsSeparableExtensionSP line 44 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra
4 instances, coercions and auxiliary constants left out.
Also declared: APNOutputs/StacksProject/GeometricallyReduced_isGeometricallyReduced_iff_of_separable_algebraic.lean:44 (same declaration text), APNOutputs/StacksProject/GeometricallyReduced_isReduced_tensorProduct_of_separable.lean:44 (same declaration text).
class IsSeparablyFinitelyGenerated line 47 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra
4 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: APNOutputs/StacksProject/GeometricallyReduced_isGeometricallyReduced_iff_of_separable_algebraic.lean:47 (same statement text; different proof or body), APNOutputs/StacksProject/GeometricallyReduced_isReduced_tensorProduct_of_separable.lean:47 (same statement text; different proof or body). Qualify references as IsSeparablyFinitelyGenerated@path.
def tensorFinsuppEquiv line 63 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, LinearEquiv, RingHom.id, TensorProduct, Finsupp, Module.Free.ChooseBasisIndex
Proof uses: Module.Basis, Module.Free.chooseBasis, TensorProduct.congr, Module.Basis.repr, LinearEquiv.refl, TensorProduct.finsuppLeft, Finsupp.mapRange.linearEquiv, TensorProduct.lid, LinearEquiv.trans
62 instances, coercions and auxiliary constants left out.
abbrev ProdResidueFields line 72 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing
Proof uses: PrimeSpectrum, HasQuotient.Quotient, Ideal, PrimeSpectrum.asIdeal
3 instances, coercions and auxiliary constants left out.
def evalMap line 75 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, LinearMap, RingHom.id, ProdResidueFields, PrimeSpectrum, HasQuotient.Quotient, Ideal, PrimeSpectrum.asIdeal
Proof uses: LinearMap.pi, AlgHom.toLinearMap, IsScalarTower.toAlgHom
42 instances, coercions and auxiliary constants left out.
lemma evalMap_injective line 79 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsReduced, Function.Injective, ProdResidueFields, LinearMap, RingHom.id, PrimeSpectrum, HasQuotient.Quotient, Ideal, PrimeSpectrum.asIdeal, evalMap
Proof uses: id, Eq, Iff.mp, HSub.hSub, OfNat.ofNat, sub_eq_zero, IsReduced.eq_zero, Iff.mpr, IsNilpotent, Ideal.IsPrime, Membership.mem, nilpotent_iff_mem_prime, RingHom, Ideal.Quotient.mk, Ideal.Quotient.eq, congrFun, PrimeSpectrum.mk
83 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma tensor_map_injective line 84 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, AddCommGroup, Module, LinearMap, RingHom.id, Function.Injective, TensorProduct, TensorProduct.map, LinearMap.id
Proof uses: Module.Flat.lTensor_preserves_injective_linearMap
60 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: APNOutputs/StacksProject/AlgebrasOverFields_unique_minimal_prime_of_tensor_product_of_separably_closed.lean:347 (different declaration text). Qualify references as tensor_map_injective@path.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def mapToS line 90 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, LinearMap, RingHom.id, TensorProduct
Proof uses: LinearMap.comp, TensorProduct.lid, TensorProduct.map, LinearMap.id
51 instances, coercions and auxiliary constants left out.
lemma mapToS_eval line 94 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, LinearMap, RingHom.id, TensorProduct, PrimeSpectrum, Eq, HasQuotient.Quotient, Ideal, PrimeSpectrum.asIdeal, RingHom, Ideal.Quotient.mk, mapToS, TensorProduct.map, LinearMap.id, AlgHom.toLinearMap, IsScalarTower.toAlgHom
Proof uses: TensorProduct.induction_on, Eq.refl, OfNat.ofNat, TensorProduct.tmul, of_eq_true, HAdd.hAdd, Eq.trans, True, congr, congrArg, map_add, eq_self
94 instances, coercions and auxiliary constants left out.
Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma tensorFinsuppEquiv_apply_eq_mapToS line 100 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, TensorProduct, Module.Free.ChooseBasisIndex, Eq, Finsupp, LinearEquiv, RingHom.id, tensorFinsuppEquiv, LinearMap, mapToS, Module.Basis.coord, Module.Free.chooseBasis
Proof uses: TensorProduct.induction_on, Eq.refl, OfNat.ofNat, Eq.mpr, TensorProduct.tmul, HSMul.hSMul, Module.Basis.repr, id, congrArg, TensorProduct.finsuppLeft, TensorProduct.lid, TensorProduct.finsuppLeft_apply_tmul_apply, of_eq_true, HAdd.hAdd, Eq.trans, True, congr, map_add, eq_self
103 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma tensor_eq_zero_of_mapToS_eq_zero line 107 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, TensorProduct, LinearMap, RingHom.id, Eq, mapToS, OfNat.ofNat
Proof uses: Finsupp, Module.Free.ChooseBasisIndex, LinearEquiv, tensorFinsuppEquiv, Finsupp.ext, Eq.mpr, id, congrArg, Finsupp.zero_apply, Module.Basis.coord, Module.Free.chooseBasis, tensorFinsuppEquiv_apply_eq_mapToS, Iff.mp, LinearEquiv.map_eq_zero_iff
71 instances, coercions and auxiliary constants left out.
Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma tensor_eq_zero_of_eval_eq_zero line 116 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsReduced, TensorProduct, PrimeSpectrum, Eq, HasQuotient.Quotient, Ideal, PrimeSpectrum.asIdeal, LinearMap, RingHom.id, TensorProduct.map, LinearMap.id, AlgHom.toLinearMap, IsScalarTower.toAlgHom, OfNat.ofNat
Proof uses: tensor_eq_zero_of_mapToS_eq_zero, RingHom, Ideal.Quotient.mk, mapToS, Eq.mpr, id, congrArg, mapToS_eval, map_zero, Function.comp, Ideal.IsPrime, Membership.mem, IsNilpotent, IsReduced.eq_zero, Iff.mpr, nilpotent_iff_mem_prime, Iff.mp, PrimeSpectrum.mk, Ideal.Quotient.eq_zero_iff_mem
98 instances, coercions and auxiliary constants left out.
Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma map_injective_of_fractionRing line 132 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsDomain, Function.Injective, TensorProduct, FractionRing, nonZeroDivisors, LinearMap, RingHom.id, TensorProduct.map, LinearMap.id, AlgHom.toLinearMap, IsScalarTower.toAlgHom
Proof uses: Module.Flat.lTensor_preserves_injective_linearMap, of_eq_true, Eq, Eq.trans, True, forall_congr, implies_congr_ctx, congrArg, eq_self, implies_true
100 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma isReduced_quotient_of_coprime line 137 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Polynomial, IsCoprime, LinearMap, RingHom.id, Polynomial.derivative, IsReduced, HasQuotient.Quotient, Ideal, Ideal.span, Singleton.singleton, Set
Proof uses: Eq.mpr, IsNilpotent, Eq, OfNat.ofNat, id, Iff.mpr, RingHom, Ideal.Quotient.mk, Function.Surjective.forall, Ideal.Quotient.mk_surjective, Function.comp, Dvd.dvd, Membership.mem, Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton, by_contra, Not, absurd, HPow.hPow, Nat and 63 more
123 instances, coercions and auxiliary constants left out.
Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma isReduced_quotient_of_separable line 150 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Polynomial, Polynomial.Separable, IsReduced, HasQuotient.Quotient, Ideal, Ideal.span, Singleton.singleton, Set
Proof uses: IsCoprime, LinearMap, RingHom.id, Polynomial.derivative, isReduced_quotient_of_coprime
34 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma quotient_map_injective_cond line 155 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, RingHom, Polynomial, Membership.mem, Ideal, Ideal.span, Singleton.singleton, Set, Eq, HasQuotient.Quotient, Polynomial.map, RingHom.comp, Ideal.Quotient.mk, Polynomial.mapRingHom, OfNat.ofNat
Proof uses: HMul.hMul, Dvd.dvd, Iff.mp, Ideal.mem_span_singleton, Eq.mpr, id, congrArg, map_mul, Ideal.mem_span_singleton_self, Iff.mpr, Ideal.Quotient.eq_zero_iff_mem, of_eq_true, Eq.trans, True, MulZeroClass.zero_mul, eq_self
68 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma modByMonic_sub_mem_ideal line 164 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Polynomial, Polynomial.Monic, Membership.mem, Ideal, Ideal.span, Singleton.singleton, Set, HSub.hSub, Polynomial.modByMonic
Proof uses: Eq, HAdd.hAdd, HMul.hMul, Polynomial.divByMonic, Polynomial.modByMonic_add_div, Trans.trans, Eq.mpr, id, congrArg, Eq.refl, add_sub_cancel_left, Iff.mpr, Dvd.dvd, Ideal.mem_span_singleton, Exists.intro, rfl
50 instances, coercions and auxiliary constants left out.
Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma zero_of_mem_span_of_degree_lt line 173 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Polynomial, Polynomial.Monic, Membership.mem, Ideal, Ideal.span, Singleton.singleton, Set, Or, Eq, OfNat.ofNat, LT.lt, WithBot, Nat, Polynomial.degree
Proof uses: HMul.hMul, Dvd.dvd, Iff.mp, Ideal.mem_span_singleton, Or.inl, Or.inr, Ne, Classical.em, Eq.mp, congrArg, MulZeroClass.mul_zero, HAdd.hAdd, Polynomial.Monic.degree_mul, mul_comm, Eq.mpr, id, Eq.symm, False, LT.lt.not_ge, Eq.rec and 5 more
70 instances, coercions and auxiliary constants left out.
Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma polynomial_quotient_map_prod_injective_cond line 193 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, RingHom, Eq, OfNat.ofNat, Polynomial, Polynomial.Monic, Membership.mem, Ideal, Ideal.span, Singleton.singleton, Set, Polynomial.map
Proof uses: Polynomial.modByMonic, HSub.hSub, modByMonic_sub_mem_ideal, Polynomial.ext, Nat, Polynomial.coeff, by_contra, Not, absurd, Dvd.dvd, False, Dvd.dvd.sub, Iff.mp, Ideal.mem_span_singleton, Polynomial.map_dvd, Eq.mpr, HMul.hMul, id, Eq.trans, Exists and 53 more
97 instances, coercions and auxiliary constants left out.
Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma polynomial_quotient_map_prod_injective line 216 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, RingHom, Eq, OfNat.ofNat, Polynomial, Polynomial.Monic, Function.Injective, HasQuotient.Quotient, Ideal, Ideal.span, Singleton.singleton, Set, Polynomial.map, Ideal.Quotient.lift, RingHom.comp, Ideal.Quotient.mk, Polynomial.mapRingHom, quotient_map_injective_cond
Proof uses: Quotient.inductionOn₂', Submodule.quotientRel, Quotient.mk'', Membership.mem, HSub.hSub, congr_fun, Eq.mpr, id, congrArg, Polynomial.map_sub, map_sub, Iff.mpr, sub_eq_zero, Iff.mp, Ideal.Quotient.eq_zero_iff_mem, polynomial_quotient_map_prod_injective_cond, Ideal.Quotient.eq
70 instances, coercions and auxiliary constants left out.
Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma isReduced_quotient_of_monic_separable_prod line 241 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Field, RingHom, Eq, OfNat.ofNat, Polynomial, Polynomial.Monic, Polynomial.Separable, Polynomial.map, IsReduced, HasQuotient.Quotient, Ideal, Ideal.span, Singleton.singleton, Set
Proof uses: Function.Injective, Ideal.Quotient.lift, RingHom.comp, Ideal.Quotient.mk, Polynomial.mapRingHom, quotient_map_injective_cond, polynomial_quotient_map_prod_injective, IsReduced.mk, IsNilpotent, Nat, HPow.hPow, Eq.mpr, id, congrArg, map_zero, Eq.refl, Eq.symm, map_pow, Exists.intro, IsReduced.eq_zero and 2 more
77 instances, coercions and auxiliary constants left out.
Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
lemma isReduced_polynomial_quotient_of_monic_separable line 287 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsReduced, Polynomial, Polynomial.Monic, Polynomial.Separable, HasQuotient.Quotient, Ideal, Ideal.span, Singleton.singleton, Set, Polynomial.map, algebraMap
Proof uses: PrimeSpectrum, FractionRing, PrimeSpectrum.asIdeal, RingHom, nonZeroDivisors, RingHom.comp, Ideal.Quotient.mk, Eq, OfNat.ofNat, Function.Injective, IsFractionRing.injective, Eq.mpr, id, congrArg, map_zero, Membership.mem, Iff.mp, Ideal.Quotient.eq_zero_iff_mem, IsNilpotent, nilradical and 15 more
83 instances, coercions and auxiliary constants left out.
Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
lemma isReduced_localization line 319 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Submonoid, IsLocalization, IsReduced
Proof uses: IsReduced.mk, IsNilpotent, isReduced_localization.match_1, Eq, OfNat.ofNat, Nat, HPow.hPow, Nat.casesAuxOn, Eq.mp, congrArg, pow_zero, eq_zero_of_zero_eq_one, Eq.symm, HAdd.hAdd, Prod, Subtype, Membership.mem, HMul.hMul, RingHom, algebraMap and 31 more
71 instances, coercions and auxiliary constants left out.
Tactic trace: 44 steps
Open to load the checked before-and-after goal states.
lemma alg_equiv_reduced line 369 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, AlgEquiv, IsReduced
Proof uses: isReduced_of_injective, AlgHom, AlgEquiv.injective
28 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def TensorProduct_isReduced_of_primitive_element_aux_equiv_to line 373 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, AlgHom, Polynomial, TensorProduct
Proof uses: Algebra.TensorProduct.rightAlgebra, Polynomial.aeval, TensorProduct.tmul, OfNat.ofNat, AlgHom.restrictScalars
53 instances, coercions and auxiliary constants left out.
lemma TensorProduct_isReduced_of_primitive_element_aux_equiv_to_ker line 380 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Membership.mem, Polynomial, Ideal, RingHom.ker, TensorProduct, RingHom, AlgHom.toRingHom, TensorProduct_isReduced_of_primitive_element_aux_equiv_to, Polynomial.map, algebraMap, minpoly
Proof uses: Eq, AlgHom, OfNat.ofNat, Eq.mpr, Polynomial.aeval, TensorProduct.tmul, id, congrArg, Algebra.TensorProduct.rightAlgebra, Polynomial.aeval_map_algebraMap, Mathlib.Tactic.LinearCombination'.eq_trans₃, minpoly.aeval, of_eq_true, Eq.trans, True, Finset.sum, Nat, Finset.range, HAdd.hAdd, Polynomial.natDegree and 15 more
93 instances, coercions and auxiliary constants left out.
Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma K_equiv_polynomial_dummy line 389 source
no axioms what this means
Statement uses: True
Proof uses: trivial
lemma tensorProduct_isReduced_of_finite_separable_map_ker line 391 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsReduced, TensorProduct, IsScalarTower, AlgHom, Polynomial, Eq, Polynomial.aeval, TensorProduct.tmul, OfNat.ofNat, LE.le, Ideal, Ideal.span, Singleton.singleton, Set, Polynomial.map, algebraMap, minpoly and 1 more
Proof uses: Eq.rec, Iff.mpr, HasSubset.Subset, Ideal.span_le, Membership.mem, Eq.trans, Polynomial.aeval_map_algebraMap, Mathlib.Tactic.LinearCombination'.eq_trans₃, congr_arg, minpoly.aeval, of_eq_true, True, Finset.sum, Nat, Finset.range, HAdd.hAdd, Polynomial.natDegree, HSMul.hSMul, Polynomial.coeff, HPow.hPow and 14 more
124 instances, coercions and auxiliary constants left out.
Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def tensorProduct_isReduced_of_finite_separable_map line 398 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsReduced, AlgHom, HasQuotient.Quotient, Polynomial, Ideal, Ideal.span, Singleton.singleton, Set, Polynomial.map, algebraMap, minpoly, TensorProduct
Proof uses: Algebra.TensorProduct.rightAlgebra, Polynomial.aeval, TensorProduct.tmul, OfNat.ofNat, Ideal.Quotient.liftₐ, AlgHom.restrictScalars
76 instances, coercions and auxiliary constants left out.
def K_equiv_polynomial line 407 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, FiniteDimensional, Eq, IntermediateField, IntermediateField.adjoin, Singleton.singleton, Set, Top.top, AlgEquiv, HasQuotient.Quotient, Polynomial, Ideal, Ideal.span, minpoly
Proof uses: IsIntegral, Subtype, Membership.mem, IntermediateField.adjoinRootEquivAdjoin, AlgEquiv.trans, IntermediateField.equivOfEq, IntermediateField.topEquiv
70 instances, coercions and auxiliary constants left out.
Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma K_equiv_polynomial_apply_X line 416 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, FiniteDimensional, Eq, IntermediateField, IntermediateField.adjoin, Singleton.singleton, Set, Top.top, AlgEquiv, HasQuotient.Quotient, Polynomial, Ideal, Ideal.span, minpoly, K_equiv_polynomial, RingHom, Ideal.Quotient.mk, Polynomial.X
Proof uses: id, Membership.mem, Subalgebra, IntermediateField.toSubalgebra, Subtype, IntermediateField.adjoinRootEquivAdjoin, congr_arg, AlgHom, Polynomial.aeval, IntermediateField.AdjoinSimple.gen, Polynomial.aeval_X
98 instances, coercions and auxiliary constants left out.
Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def tensorProduct_isReduced_of_finite_separable_inv_K line 422 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsReduced, FiniteDimensional, Eq, IntermediateField, IntermediateField.adjoin, Singleton.singleton, Set, Top.top, AlgHom, HasQuotient.Quotient, Polynomial, Ideal, Ideal.span, Polynomial.map, algebraMap, minpoly
Proof uses: AlgEquiv, K_equiv_polynomial, AlgHom.comp, Ideal.Quotient.mkₐ, Polynomial.mapAlgHom, Algebra.ofId, LE.le, RingHom.ker, Ideal.Quotient.liftₐ, AlgEquiv.symm
98 instances, coercions and auxiliary constants left out.
Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
def tensorProduct_isReduced_of_finite_separable_inv line 438 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsReduced, FiniteDimensional, Eq, IntermediateField, IntermediateField.adjoin, Singleton.singleton, Set, Top.top, AlgHom, TensorProduct, HasQuotient.Quotient, Polynomial, Ideal, Ideal.span, Polynomial.map, algebraMap, minpoly
Proof uses: tensorProduct_isReduced_of_finite_separable_inv_K, Algebra.ofId, AlgHom.restrictScalars, Commute, Algebra.TensorProduct.lift
93 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma tensorProduct_isReduced_of_finite_separable_inv_inj_left line 448 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsReduced, FiniteDimensional, Eq, IntermediateField, IntermediateField.adjoin, Singleton.singleton, Set, Top.top, AlgHom, TensorProduct, AlgHom.comp, HasQuotient.Quotient, Polynomial, Ideal, Ideal.span, Polynomial.map, algebraMap and 4 more
Proof uses: id, Eq.mpr, tensorProduct_isReduced_of_finite_separable_inv_K, Algebra.ofId, AlgHom.restrictScalars, Commute, Algebra.TensorProduct.lift, Algebra.TensorProduct.rightAlgebra, Ideal.Quotient.liftₐ, Polynomial.aeval, TensorProduct.tmul, OfNat.ofNat, Ideal.Quotient.mkₐ, Polynomial.mapAlgHom, AlgEquiv, AlgEquiv.symm, K_equiv_polynomial, congrArg, Eq.refl, Algebra.TensorProduct.lift_comp_includeLeft and 66 more
183 instances, coercions and auxiliary constants left out.
Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma tensorProduct_isReduced_of_finite_separable_inv_inj_right line 465 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsReduced, FiniteDimensional, Eq, IntermediateField, IntermediateField.adjoin, Singleton.singleton, Set, Top.top, AlgHom, TensorProduct, AlgHom.comp, HasQuotient.Quotient, Polynomial, Ideal, Ideal.span, Polynomial.map, algebraMap and 4 more
Proof uses: Eq.mpr, RingHom, Algebra.TensorProduct.rightAlgebra, TensorProduct.tmul, OfNat.ofNat, id, Eq.trans, AlgHom.restrictScalars, Ideal.Quotient.liftₐ, Polynomial.aeval, Algebra.TensorProduct.lift, tensorProduct_isReduced_of_finite_separable_inv_K, Algebra.ofId, congrArg, Algebra.TensorProduct.lift_comp_includeRight', forall_congr, AlgHom.commutes, Eq.refl
117 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma tensorProduct_isReduced_of_finite_separable_inv_inj_comp line 470 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsReduced, FiniteDimensional, Eq, IntermediateField, IntermediateField.adjoin, Singleton.singleton, Set, Top.top, AlgHom, TensorProduct, AlgHom.comp, HasQuotient.Quotient, Polynomial, Ideal, Ideal.span, Polynomial.map, algebraMap and 4 more
Proof uses: Algebra.TensorProduct.ext, tensorProduct_isReduced_of_finite_separable_inv_inj_left, tensorProduct_isReduced_of_finite_separable_inv_inj_right
97 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma tensorProduct_isReduced_of_finite_separable_inv_inj line 476 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsReduced, FiniteDimensional, Eq, IntermediateField, IntermediateField.adjoin, Singleton.singleton, Set, Top.top, Function.Injective, TensorProduct, HasQuotient.Quotient, Polynomial, Ideal, Ideal.span, Polynomial.map, algebraMap, minpoly and 2 more
Proof uses: tensorProduct_isReduced_of_finite_separable_map, Eq.mpr, id, congrArg, Eq.refl, AlgHom.comp, AlgHom.id, tensorProduct_isReduced_of_finite_separable_inv_inj_comp, Eq.symm
90 instances, coercions and auxiliary constants left out.
Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma TensorProduct_isReduced_of_finite_separable line 492 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsReduced, FiniteDimensional, Algebra.IsSeparable, TensorProduct
Proof uses: Eq, IntermediateField, IntermediateField.adjoin, Singleton.singleton, Set, Top.top, Exists, Field.exists_primitive_element, Function.Injective, HasQuotient.Quotient, Polynomial, Ideal, Ideal.span, Polynomial.map, algebraMap, minpoly, AlgHom, tensorProduct_isReduced_of_finite_separable_inv, tensorProduct_isReduced_of_finite_separable_inv_inj, Polynomial.Monic and 6 more
90 instances, coercions and auxiliary constants left out.
Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma IsReduced.of_subalgebra_field_aux_fin line 504 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsAlgebraic, Subalgebra, Subalgebra.FG, FiniteDimensional, Subtype, Membership.mem
Proof uses: Exists.rec, Finset, Eq, Algebra.adjoin, Submodule, OrderEmbedding, Subalgebra.toSubmodule, Eq.rec, Iff.mpr, Module.Finite, Submodule.FG, Module.Finite.iff_fg, fg_adjoin_of_finite, Finset.finite_toSet, Set, Algebra.IsIntegral.isIntegral
50 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma IsReduced.of_subalgebra_field_aux_sep line 508 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsSeparable, Subalgebra, Subtype, Membership.mem
Proof uses: Algebra.IsSeparable.mk, Exists.imp, Polynomial, Exists, Eq, HAdd.hAdd, HMul.hMul, minpoly, LinearMap, RingHom.id, Polynomial.derivative, OfNat.ofNat, Eq.mpr, RingHom, algebraMap, id, congrArg, Eq.symm, minpoly.algebraMap_eq, Subtype.coe_injective and 1 more
53 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma IsReduced.of_subalgebra_field_aux_alg line 511 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsAlgebraic, Subalgebra, Subtype, Membership.mem
Proof uses: Algebra.IsAlgebraic.mk, Exists.imp, Polynomial, And, Ne, OfNat.ofNat, Eq, AlgHom, Polynomial.aeval, of_eq_true, Not, Eq.trans, True, forall_congr, Finset.sum, Nat, Finset.range, HAdd.hAdd, Polynomial.natDegree, HSMul.hSMul and 17 more
72 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma IsReduced.of_subalgebra_field line 513 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsReduced, Algebra.IsSeparable, Algebra.IsAlgebraic, Subalgebra, Subalgebra.FG, TensorProduct, Subtype, Membership.mem
Proof uses: IsReduced.of_subalgebra_field_aux_alg, IsField, Subalgebra.isField_of_algebraic, IsField.toField, FiniteDimensional, IsReduced.of_subalgebra_field_aux_fin, IsReduced.of_subalgebra_field_aux_sep, AlgEquiv, Algebra.TensorProduct.comm, TensorProduct_isReduced_of_finite_separable, alg_equiv_reduced
69 instances, coercions and auxiliary constants left out.
Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma isReduced_tensorProduct_of_isSeparable line 527 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Algebra.IsSeparable, Algebra.IsAlgebraic, IsReduced, TensorProduct
Proof uses: AlgEquiv, Algebra.TensorProduct.comm, IsReduced.tensorProduct_of_flat_of_forall_fg, Subalgebra, Subalgebra.FG, IsReduced.of_subalgebra_field, alg_equiv_reduced
71 instances, coercions and auxiliary constants left out.
Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma mvPolynomial_tensor_equiv_comm line 536 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, MvPolynomial, Commute, AlgHom, MvPolynomial.aeval, MvPolynomial.X, IsScalarTower.toAlgHom
Proof uses: mul_comm
58 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def mvPolynomial_tensor_equiv_lift line 540 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, AlgHom, TensorProduct, MvPolynomial
Proof uses: Algebra.TensorProduct.lift, MvPolynomial.aeval, MvPolynomial.X, IsScalarTower.toAlgHom, mvPolynomial_tensor_equiv_comm
26 instances, coercions and auxiliary constants left out.
def mvPolynomial_tensor_equiv_inv line 543 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, AlgHom, MvPolynomial, TensorProduct
Proof uses: AlgHom.restrictScalars, Algebra.TensorProduct.rightAlgebra, MvPolynomial.aeval, TensorProduct.tmul, MvPolynomial.X, OfNat.ofNat
42 instances, coercions and auxiliary constants left out.
lemma mvPolynomial_tensor_equiv_comp1 line 547 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Eq, AlgHom, MvPolynomial, AlgHom.comp, TensorProduct, mvPolynomial_tensor_equiv_lift, mvPolynomial_tensor_equiv_inv, AlgHom.id
Proof uses: AlgHom.ext, id, Eq.mpr, Algebra.TensorProduct.lift, MvPolynomial.aeval, MvPolynomial.X, IsScalarTower.toAlgHom, mvPolynomial_tensor_equiv_comm, Algebra.TensorProduct.rightAlgebra, TensorProduct.tmul, OfNat.ofNat, Finset.sum, Finsupp, Nat, MvPolynomial.support, HMul.hMul, RingHom, algebraMap, MvPolynomial.coeff, LinearMap and 44 more
102 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma mvPolynomial_tensor_equiv_comp2 line 554 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Eq, AlgHom, TensorProduct, MvPolynomial, AlgHom.comp, mvPolynomial_tensor_equiv_inv, mvPolynomial_tensor_equiv_lift, AlgHom.id
Proof uses: Algebra.TensorProduct.ext, MvPolynomial.algHom_ext, Algebra.TensorProduct.includeLeft, of_eq_true, Algebra.TensorProduct.rightAlgebra, MvPolynomial.aeval, TensorProduct.tmul, MvPolynomial.X, OfNat.ofNat, HMul.hMul, Eq.trans, True, congrArg, MvPolynomial.aeval_X, mul_one, eq_self, AlgHom.ext, AlgHom.restrictScalars, Algebra.TensorProduct.includeRight, Eq.mpr and 8 more
76 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma mvPolynomial_tensor_equiv line 561 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, Nonempty, AlgEquiv, TensorProduct, MvPolynomial
Proof uses: Nonempty.intro, AlgEquiv.ofAlgHom, mvPolynomial_tensor_equiv_lift, mvPolynomial_tensor_equiv_inv, mvPolynomial_tensor_equiv_comp1, mvPolynomial_tensor_equiv_comp2
36 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma isReduced_tensorProduct_adjoin_transcendenceBasis_aux1 line 565 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Set, IsTranscendenceBasis, Membership.mem, Nonempty, AlgEquiv, MvPolynomial, Subtype, Subalgebra, Algebra.adjoin
Proof uses: Eq.rec, AlgHom.range, MvPolynomial.aeval, Eq, Nonempty.intro, AlgEquiv.ofInjective, And.left, AlgebraicIndependent, AlgebraicIndepOn, id, HasSubset.Subset, Set.range, Eq.symm, Algebra.adjoin_eq_range
36 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma isReduced_tensorProduct_adjoin_transcendenceBasis_aux2 line 570 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Set, IsTranscendenceBasis, Membership.mem, IsReduced, TensorProduct, Subtype, Subalgebra, Algebra.adjoin
Proof uses: Nonempty, AlgEquiv, MvPolynomial, isReduced_tensorProduct_adjoin_transcendenceBasis_aux1, Algebra.TensorProduct.congr, AlgEquiv.symm, AlgEquiv.refl, Classical.choice, mvPolynomial_tensor_equiv, IsReduced.mk, IsNilpotent, Nat, Eq, HPow.hPow, OfNat.ofNat, IsNilpotent.eq_zero, Exists.intro, alg_equiv_reduced
95 instances, coercions and auxiliary constants left out.
Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma tensor_localization_isReduced_aux1 line 588 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsDomain, IsScalarTower, IsFractionRing, Function.Injective, TensorProduct, AlgHom, Algebra.TensorProduct.map, IsScalarTower.toAlgHom, AlgHom.id
Proof uses: Module.Flat.rTensor_preserves_injective_linearMap, AlgHom.toLinearMap, IsFractionRing.injective
65 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma tensor_localization_isReduced_aux2 line 594 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsDomain, IsScalarTower, IsFractionRing, Ne, OfNat.ofNat, IsUnit, TensorProduct, TensorProduct.tmul, RingHom, algebraMap
Proof uses: nonZeroDivisors, IsLocalization', Eq, Submonoid.IsLocalizationMap, IsLocalization'.mk, Subtype, Membership.mem, Submonoid, Exists, Prod, HMul.hMul, Prod.snd, Prod.fst, Submonoid.IsLocalizationMap.mk, Units, Subtype.mk, of_eq_true, Eq.trans, True, Not and 21 more
94 instances, coercions and auxiliary constants left out.
Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma exists_mul_mem_tensor_of_fractionRing_aux line 608 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsDomain, IsScalarTower, IsFractionRing, TensorProduct, Exists, Ne, OfNat.ofNat, Eq, HMul.hMul, TensorProduct.tmul, RingHom, algebraMap, AlgHom, Algebra.TensorProduct.map, IsScalarTower.toAlgHom, AlgHom.id
Proof uses: nonZeroDivisors, IsLocalization', Submonoid.IsLocalizationMap, IsLocalization'.mk, Subtype, Membership.mem, Submonoid, IsUnit, Prod, Prod.snd, Prod.fst, Submonoid.IsLocalizationMap.mk, TensorProduct.induction_on, Exists.intro, one_ne_zero, MulZeroClass.zero_mul, Prod.mk, nonZeroDivisors.ne_zero, Subtype.property, of_eq_true and 26 more
141 instances, coercions and auxiliary constants left out.
Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma tensor_localization_isReduced line 624 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsDomain, IsScalarTower, IsFractionRing, IsReduced, TensorProduct
Proof uses: IsReduced.mk, IsNilpotent, tensor_localization_isReduced.match_1, Eq, OfNat.ofNat, Nat, HPow.hPow, Exists, Ne, HMul.hMul, TensorProduct.tmul, RingHom, algebraMap, AlgHom, Algebra.TensorProduct.map, IsScalarTower.toAlgHom, AlgHom.id, exists_mul_mem_tensor_of_fractionRing_aux, Eq.mpr, id and 15 more
92 instances, coercions and auxiliary constants left out.
Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
instance adjoin_algebra_adjoin line 648 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Set, Subtype, Membership.mem, Subalgebra, Algebra.adjoin, IntermediateField, IntermediateField.adjoin
Proof uses: RingHom.toAlgebra, AlgHom, IntermediateField.toSubalgebra, Subalgebra.inclusion
27 instances, coercions and auxiliary constants left out.
lemma isScalarTower_adjoin line 652 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Set, IsScalarTower, Subtype, Membership.mem, Subalgebra, Algebra.adjoin, IntermediateField, IntermediateField.adjoin
Proof uses: IsScalarTower.mk, Subtype.eq, HSMul.hSMul, Algebra.smul_mul_assoc, SubMulAction, Submodule.toSubMulAction, OrderEmbedding, Submodule, Subalgebra.toSubmodule
85 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma isFractionRing_adjoin_map_units line 656 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Set, Subtype, Membership.mem, Subalgebra, Algebra.adjoin, Submonoid, nonZeroDivisors, IsUnit, IntermediateField, IntermediateField.adjoin, RingHom, algebraMap
Proof uses: Ne.isUnit, Function.comp, Eq, OfNat.ofNat, False, nonZeroDivisors.ne_zero, Subtype.property, Subtype.eq, congr_arg
53 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma isFractionRing_adjoin_surj line 660 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Set, Subtype, Membership.mem, IntermediateField, IntermediateField.adjoin, Exists, Prod, Subalgebra, Algebra.adjoin, Submonoid, nonZeroDivisors, Eq, HMul.hMul, RingHom, algebraMap, Prod.snd, Prod.fst
Proof uses: Eq.mpr, And, Not, Subtype.mk, OfNat.ofNat, Mul.mul, id, Eq.trans, Prod.mk, congrArg, funext, propext, exists_prop_congr, Iff.of_eq, Eq.refl, Ne, Subtype.property, MvPolynomial, HDiv.hDiv, AlgHom and 41 more
143 instances, coercions and auxiliary constants left out.
Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma isFractionRing_adjoin_eq_iff_exists line 674 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Set, Subtype, Membership.mem, Subalgebra, Algebra.adjoin, Eq, IntermediateField, IntermediateField.adjoin, RingHom, algebraMap, Exists, Submonoid, nonZeroDivisors, HMul.hMul
Proof uses: Exists.intro, Subtype.mk, OfNat.ofNat, OneMemClass.one_mem, congr_arg, Subtype.eq, Iff.mp, And, and_self_iff, Eq.mpr, id, Eq.trans, congr, congrArg, and_self, Subtype.mk.inj, IntermediateField.toSubalgebra, Algebra.algebraMap
70 instances, coercions and auxiliary constants left out.
Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma isFractionRing_adjoin line 681 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Set, IsFractionRing, Subtype, Membership.mem, Subalgebra, Algebra.adjoin, IntermediateField, IntermediateField.adjoin
Proof uses: IsLocalization'.mk, nonZeroDivisors, Submonoid.IsLocalizationMap.mk, RingHom, algebraMap, isFractionRing_adjoin_map_units, isFractionRing_adjoin_surj, isFractionRing_adjoin_eq_iff_exists
36 instances, coercions and auxiliary constants left out.
lemma isReduced_tensorProduct_adjoin_transcendenceBasis line 687 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Set, IsTranscendenceBasis, Membership.mem, IsReduced, TensorProduct, Subtype, IntermediateField, IntermediateField.adjoin
Proof uses: Subalgebra, Algebra.adjoin, isReduced_tensorProduct_adjoin_transcendenceBasis_aux2, tensor_localization_isReduced, inferInstance, IsDomain, isScalarTower_adjoin, isFractionRing_adjoin
86 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def tensor_equiv_base_change_f line 696 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, AlgHom, TensorProduct
Proof uses: AlgHom.restrictScalars, Algebra.TensorProduct.includeLeft, AlgHom.comp, Algebra.TensorProduct.includeRight, Commute, Algebra.TensorProduct.lift
78 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def tensor_equiv_base_change_g line 709 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, AlgHom, TensorProduct
Proof uses: Algebra.TensorProduct.includeLeft, AlgHom.mk, AlgHom.toRingHom, Algebra.TensorProduct.map, IsScalarTower.toAlgHom, AlgHom.id, Commute, Algebra.TensorProduct.lift
68 instances, coercions and auxiliary constants left out.
lemma tensor_equiv_base_change_gf line 725 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, TensorProduct, Eq, AlgHom, tensor_equiv_base_change_g, tensor_equiv_base_change_f
Proof uses: id, TensorProduct.induction_on, Algebra.TensorProduct.lift, AlgHom.mk, AlgHom.toRingHom, Algebra.TensorProduct.includeLeft, Algebra.TensorProduct.map, IsScalarTower.toAlgHom, AlgHom.id, AlgHom.restrictScalars, AlgHom.comp, Algebra.TensorProduct.includeRight, RingHom.map_zero, of_eq_true, RingHom, OneHom.toFun, algebraMap, Eq.refl, Commute, TensorProduct.tmul and 13 more
117 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma tensor_equiv_base_change line 733 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsScalarTower, IsReduced, TensorProduct
Proof uses: Function.Injective, AlgHom, tensor_equiv_base_change_f, Function.LeftInverse.injective, tensor_equiv_base_change_g, tensor_equiv_base_change_gf, isReduced_of_injective
74 instances, coercions and auxiliary constants left out.
Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma isReduced_tensorProduct_field_of_separablyGenerated line 744 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, IsSeparablyGenerated, IsReduced, TensorProduct
Proof uses: Set, And, IsTranscendenceBasis, Membership.mem, Algebra.IsSeparable, Subtype, IntermediateField, IntermediateField.adjoin, Exists, IsSeparablyGenerated.out, isReduced_tensorProduct_adjoin_transcendenceBasis, tensor_equiv_base_change, isReduced_tensorProduct_of_isSeparable, inferInstance, Algebra.IsAlgebraic
80 instances, coercions and auxiliary constants left out.
Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
theorem isReduced_tensorProduct_of_separablyGenerated line 760 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsSeparablyGenerated, IsReduced, TensorProduct
Proof uses: IsReduced.mk, IsNilpotent, Nat, Eq, HPow.hPow, OfNat.ofNat, tensor_eq_zero_of_eval_eq_zero, PrimeSpectrum, HasQuotient.Quotient, Ideal, PrimeSpectrum.asIdeal, FractionRing, nonZeroDivisors, isReduced_tensorProduct_field_of_separablyGenerated, Function.Injective, LinearMap, RingHom.id, TensorProduct.map, LinearMap.id, AlgHom.toLinearMap and 29 more
122 instances, coercions and auxiliary constants left out.
Tactic trace: 22 steps
Open to load the checked before-and-after goal states.