Theorems · Theorem · linear algebra
Module.Basis.repr_self_apply
∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(b : Module.Basis ι R M) (i j : ι) [inst_3 : Decidable (i = j)], (b.repr (b i)) j = if i = j then 1 else 0- Defined in
- Mathlib.LinearAlgebra.Basis.Defs
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Modulestatement and proof · cited by 20,661
- RingHom.idstatement · cited by 18,349
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- Finsuppstatement and proof · cited by 5,255
- LinearEquivstatement · cited by 3,317
- Module.Basisstatement and proof · cited by 1,477
- Module.Basis.reprstatement · cited by 498
- Finsupp.single_applyproof · cited by 99
- Module.Basis.repr_selfproof · cited by 82
Cited by9
Results whose statement or proof uses this declaration.
- WeierstrassCurve.Affine.CoordinateRing.norm_smul_basisproof · cited by 2
- PowerBasis.repr_gen_pow_isIntegralproof · cited by 2
- LinearMap.polyCharpolyAux_baseChangeproof · cited by 2
- ClassGroup.exists_mem_finsetApproxproof · cited by 1
- Module.Basis.equivFun_selfproof · cited by 1
- IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_pow_ne_twoproof · cited by 1
- PowerBasis.repr_pow_isIntegralproof · cited by 1
- contractLeft_assoc_coevaluationproof · cited by 0
- contractLeft_assoc_coevaluation'proof · cited by 0