FLT/Mathlib/Algebra/Central/TensorProduct.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma Subalgebra.sup_includeLeft_includeRight_eq_top line 30 source

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: CommSemiring, Semiring, Algebra, Eq, Subalgebra, TensorProduct, Max.max, AlgHom.range, Algebra.TensorProduct.includeLeft, Algebra.TensorProduct.includeRight, Top.top

   Proof uses: Subalgebra.ext, Eq.mpr, Iff, Membership.mem, id, Eq.trans, True, congrArg, iff_true, TensorProduct.inductionOn, TensorProduct.tmul, HMul.hMul, OfNat.ofNat, of_eq_true, congr, mul_one, one_mul, eq_self, Subalgebra.mul_mem, Algebra.mem_sup_left and 5 more

   62 instances, coercions and auxiliary constants left out.

   Tactic trace: 7 steps

   Open to load the checked before-and-after goal states.

2. lemma Subalgebra.center_tensorProduct_eq_inf line 44 source

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Field, Ring, Algebra, Eq, Subalgebra, TensorProduct, Subalgebra.center, Min.min, AlgHom.range, Subtype, Membership.mem, Algebra.TensorProduct.map, Subalgebra.val, AlgHom.id

   Proof uses: Eq.mpr, Subalgebra.centralizer, Algebra.TensorProduct.includeLeft, id, congrArg, Eq.symm, Subalgebra.centralizer_coe_range_includeLeft_eq_center_tensorProduct, Algebra.TensorProduct.includeRight, Subalgebra.centralizer_range_includeRight_eq_center_tensorProduct, Max.max, Subalgebra.centralizer_coe_sup, of_eq_true, Eq.trans, True, Set.univ, Set, Top.top, Subalgebra.sup_includeLeft_includeRight_eq_top, Subalgebra.centralizer_univ, eq_self

   70 instances, coercions and auxiliary constants left out.

   Tactic trace: 2 steps

   Open to load the checked before-and-after goal states.

3. lemma Submodule.tensorProduct_inf_eq_range_map line 55 source

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Field, AddCommGroup, Module, Submodule, Eq, TensorProduct, Min.min, LinearMap.range, Subtype, Membership.mem, RingHom.id, TensorProduct.map, Submodule.subtype, LinearMap.id

   Proof uses: le_antisymm, Set, LinearMap, Submodule.projectionOnto, Exists.choose, IsCompl, Submodule.exists_isCompl, Exists.choose_spec, LinearMap.comp, Eq.mpr, id, congrArg, Eq.symm, TensorProduct.inductionOn, of_eq_true, TensorProduct.tmul, Eq.trans, True, congrFun', Submodule.projectionOnto_apply_left and 16 more

   53 instances, coercions and auxiliary constants left out.

   Tactic trace: 21 steps

   Open to load the checked before-and-after goal states.

4. lemma Subalgebra.tensorProduct_inf_eq_range_map line 80 source

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Field, Ring, Algebra, Subalgebra, Eq, TensorProduct, Min.min, AlgHom.range, Subtype, Membership.mem, Algebra.TensorProduct.map, Subalgebra.val, AlgHom.id

   Proof uses: Subalgebra.toSubmodule_injective, Submodule.tensorProduct_inf_eq_range_map, OrderEmbedding, Submodule, Subalgebra.toSubmodule

   61 instances, coercions and auxiliary constants left out.

5. lemma Subalgebra.center_tensorProduct line 90 source

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Field, Ring, Algebra, Eq, Subalgebra, TensorProduct, Subalgebra.center, AlgHom.range, Subtype, Membership.mem, Algebra.TensorProduct.map, Subalgebra.val

   Proof uses: Min.min, AlgHom.id, Subalgebra.center_tensorProduct_eq_inf, of_eq_true, Eq.trans, True, congrFun', congrArg, id, Eq.mp, Subalgebra.tensorProduct_inf_eq_range_map, eq_self

   51 instances, coercions and auxiliary constants left out.

   Tactic trace: 11 steps

   Open to load the checked before-and-after goal states.

6. instance (instance at line 99) line 99 source