Theorems · Theorem · ring theory
LinearMap.mul_apply_apply
∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A] [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A] (m x2 : A), ((LinearMap.mul R A) m) x2 = m * x2
- Defined in
- Mathlib.Algebra.Algebra.Bilinear
- Cited by
- 25 results in Mathlib
- Foundations
- Depth 37 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
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
- CommSemiringstatement and proof · cited by 10,911
- LinearMapstatement · cited by 10,215
- IsScalarTowerstatement and proof · cited by 3,896
- SMulCommClassstatement and proof · cited by 1,927
- NonUnitalNonAssocSemiringstatement and proof · cited by 1,081
- LinearMap.mulstatement and proof · cited by 61
Cited by25
Results whose statement or proof uses this declaration.
- Ideal.absNorm_span_singletonproof · cited by 18
- Algebra.norm_selfproof · cited by 6
- Algebra.lmul_injectiveproof · cited by 5
- Algebra.trace_eq_of_algEquivproof · cited by 4
- Algebra.isEpi_iff_forall_one_tmul_eqproof · cited by 3
- Submodule.map_mulproof · cited by 3
- Algebra.norm_eq_of_algEquivproof · cited by 2
- Submodule.mem_mul_span_singletonproof · cited by 2
- Ideal.range_mulproof · cited by 2
- Module.Free.bijective_algebraMap_of_finrank_eq_oneproof · cited by 1
- Algebra.norm_eq_of_ringEquivproof · cited by 1
- matPolyEquiv_coeff_apply_aux_1proof · cited by 1