FLT/Mathlib/RingTheory/TensorProduct/Pi.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Pi

Material destined for Mathlib.

Imports (1)
Imported by 2 files
  1. theorem Algebra.TensorProduct.piScalarRight_symm_apply_of_algebraMap line 18 source

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

    Statement uses: CommSemiring, Algebra, Semiring, IsScalarTower, Fintype, DecidableEq, Eq, TensorProduct, LinearEquiv, RingHom.id, LinearEquiv.symm, TensorProduct.piScalarRight, RingHom, Algebra.algebraMap, TensorProduct.tmul, OfNat.ofNat, Finset.sum, Finset.univ, Pi.single

    Proof uses: of_eq_true, Eq.trans, HSMul.hSMul, True, congrFun', congrArg, funext, Algebra.algebraMap_eq_smul_one, LinearMap, TensorProduct.piScalarRightHom, TensorProduct.piScalarRight_apply, TensorProduct.piScalarRightHom_tmul, Finset.sum_apply, ite, Membership.mem, Finset, Finset.sum_pi_single, ite_eq_left_of_eq_true, eq_self

    61 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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