def preimage {K : Type u_1} [Field K] {V : Type u_2} [AddCommGroup V] [Module K V] {W : Type u_3} [AddCommGroup W] [Module K W] (φ : V →ₗ[K] W) (H : Submodule K W) : Submodule K V

Equations

• preimage φ H = { carrier := ⇑φ ⁻¹' ↑H, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }