theorem
L24 ↗map_apply_eq_det_smul
exteriorPower.map_apply_eq_det_smul
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.exteriorPower_map_apply_eq_det_smulLean source · statement
theorem _root_.exteriorPower.map_apply_eq_det_smul {A : Type*} [CommRing A] {M : Type*}
[AddCommGroup M]
[Module A M] {ι : Type*} [Fintype ι] (b : Module.Basis ι A M) {n : ℕ} (hn : Fintype.card ι = n)
(f : M →ₗ[A] M) (x : ⋀[A]^n M) :
exteriorPower.map n f x = LinearMap.det f • x