exteriorPower.map_mulLeft_apply_eq_norm_smul
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.exteriorPower_map_mulLeft_apply_eq_norm_smulLean source · statement
theorem _root_.exteriorPower.map_mulLeft_apply_eq_norm_smul {A B : Type*} [CommRing A] [CommRing B]
[Algebra A B]
{ι : Type*} [Fintype ι] (b : Module.Basis ι A B) {n : ℕ} (hn : Fintype.card ι = n)
(x : B) (w : ⋀[A]^n B) :
exteriorPower.map n (LinearMap.mulLeft A x) w = Algebra.norm A x • w