FLT/Mathlib/LinearAlgebra/Dimension/Constructions.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

3 declarations, 0 contain sorry, 0 declared as axioms

Constructions

Material destined for Mathlib.

Imports (4)
Imported by 3 files
  1. def Module.Finite.equivPi Choice of an R-linear isomorphism M ≃ R^(finrank R M) for a finite free module M over a ring R with the strong rank condition line 25 source

    Source documentation

    Choice of an R-linear isomorphism M ≃ R^(finrank R M) for a finite free module M over a ring R with the strong rank condition.

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

    Statement uses: Ring, StrongRankCondition, AddCommGroup, Module, Module.Free, Module.Finite, LinearEquiv, RingHom.id, Fin, Module.finrank

    Proof uses: LinearEquiv.ofFinrankEq

    17 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    noncomputable def Module.Finite.equivPi (R M : Type*) [Ring R] [StrongRankCondition R]
    [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] :
    M ≃ₗ[R] Fin (Module.finrank R M) → R :=
…
  2. abbrev TensorProduct.AlgebraTensorModule.finiteEquivPi Base change of Module.Finite.equivPi to an R-algebra N: the equivalence N ⊗[R] M ≃ₗ[N] Fin (finrank R M) → N line 32 source

    Source documentation

    Base change of Module.Finite.equivPi to an R-algebra N: the equivalence N ⊗[R] M ≃ₗ[N] Fin (finrank R M) → N.

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

    Statement uses: CommRing, CommSemiring, Ring, Algebra, Module, Module.Free, Module.Finite, StrongRankCondition, LinearEquiv, RingHom.id, TensorProduct, Fin, Module.finrank

    Proof uses: LinearEquiv.trans, TensorProduct.AlgebraTensorModule.congr, LinearEquiv.refl, Module.Finite.equivPi, TensorProduct.piScalarRight

    32 instances, coercions and auxiliary constants left out.

    noncomputable abbrev TensorProduct.AlgebraTensorModule.finiteEquivPi (R M N : Type*) [CommRing R]
    [CommSemiring N] [Ring M] [Algebra R N] [Module R M] [Module.Free R M] [Module.Finite R M]
    [StrongRankCondition R] :
    N ⊗[R] M ≃ₗ[N] Fin (Module.finrank R M) → N :=
…
  3. theorem TensorProduct.AlgebraTensorModule.finiteEquivPi_symm_apply line 39 source

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

    Statement uses: Field, CommSemiring, Ring, Algebra, Module, Module.Free, Module.Finite, StrongRankCondition, Fin, Module.finrank, Eq, TensorProduct, LinearEquiv, RingHom.id, LinearEquiv.symm, TensorProduct.AlgebraTensorModule.finiteEquivPi, RingHom, Algebra.algebraMap, TensorProduct.tmul, OfNat.ofNat and 1 more

    Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, TensorProduct.piScalarRight, TensorProduct.AlgebraTensorModule.congr, LinearEquiv.refl, Finset.sum, Finset.univ, Pi.single, Algebra.TensorProduct.piScalarRight_symm_apply_of_algebraMap, Finset.univ_sum_single, eq_self

    67 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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