K : Type u
V : Type v
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
W✝ : Subspace K V
V₁ : Type ?u.1312004
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₁
W : Subspace K V
this : dualCoannihilator (dualAnnihilator W) = W
⊢ dualAnnihilator (dualAnnihilator W) = ↑(Module.mapEvalEquiv K V) W
K : Type u
V : Type v
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
W✝ : Subspace K V
V₁ : Type ?u.1312004
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₁
W : Subspace K V
⊢ dualAnnihilator (dualAnnihilator W) = ↑(Module.mapEvalEquiv K V) W
have : _ = W := Subspace.dualAnnihilator_dualCoannihilator_eq
K : Type u
V : Type v
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
W✝ : Subspace K V
V₁ : Type ?u.1312004
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₁
W : Subspace K V
this✝ : comap (Module.Dual.eval K V) (dualAnnihilator (dualAnnihilator W)) = W
this : ↑(OrderIso.symm (Module.mapEvalEquiv K V)) (dualAnnihilator (dualAnnihilator W)) = W
⊢ dualAnnihilator (dualAnnihilator W) = ↑(Module.mapEvalEquiv K V) W
K : Type u
V : Type v
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
W✝ : Subspace K V
V₁ : Type ?u.1312004
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₁
W : Subspace K V
this : dualCoannihilator (dualAnnihilator W) = W
⊢ dualAnnihilator (dualAnnihilator W) = ↑(Module.mapEvalEquiv K V) W
rw [dualCoannihilator, ← Module.mapEvalEquiv_symm_apply] at this
no goals
K : Type u
V : Type v
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
W✝ : Subspace K V
V₁ : Type ?u.1312004
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₁
W : Subspace K V
this✝ : comap (Module.Dual.eval K V) (dualAnnihilator (dualAnnihilator W)) = W
this : ↑(OrderIso.symm (Module.mapEvalEquiv K V)) (dualAnnihilator (dualAnnihilator W)) = W
⊢ dualAnnihilator (dualAnnihilator W) = ↑(Module.mapEvalEquiv K V) W
rwa [← OrderIso.symm_apply_eq]