Theorems · Definition · ring theory
AlgEquiv.toLinearMap
{R : Type uR} →
{A₁ : Type uA₁} →
{A₂ : Type uA₂} →
[inst : CommSemiring R] →
[inst_1 : Semiring A₁] →
[inst_2 : Semiring A₂] → [inst_3 : Algebra R A₁] → [inst_4 : Algebra R A₂] → (A₁ ≃ₐ[R] A₂) → A₁ →ₗ[R] A₂Interpret an algebra equivalence as a linear map.
- Defined in
- Mathlib.Algebra.Algebra.Equiv
- Cited by
- 34 results in Mathlib
- Foundations
- Depth 24 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- RingHom.idstatement · cited by 18,349
- Semiringstatement and proof · cited by 13,802
- Algebrastatement and proof · cited by 11,388
- CommSemiringstatement and proof · cited by 10,911
- LinearMapstatement · cited by 10,215
- AlgEquivstatement and proof · cited by 1,681
- LinearEquiv.toLinearMapproof · cited by 1,171
- AlgEquiv.toLinearEquivproof · cited by 117
Cited by38
Results whose statement or proof uses this declaration.
- Algebra.QuasiFinite.transproof · cited by 8
- Module.Finite.of_quasiFiniteproof · cited by 7
- PiToModule.fromMatrixproof · cited by 6
- Algebra.FormallyUnramified.isReduced_of_fieldproof · cited by 6
- Ideal.comap_map_eq_self_of_faithfullyFlatproof · cited by 4
- PiTensorProduct.dualDistribproof · cited by 4
- AlgEquiv.eq_linearEquivConjAlgEquivproof · cited by 4
- FractionalIdeal.map_divproof · cited by 2
- minpoly_algEquiv_toLinearMapstatement and proof · cited by 2
- Submodule.map_divstatement · cited by 2
- PiTensorProduct.dualDistrib_applyproof · cited by 2
- AlgEquiv.toLinearMap_applystatement · cited by 2