case mp
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W W' : Subspace K V
⊢ dualAnnihilator W = dualAnnihilator W' → W = W'

case mpr
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W W' : Subspace K V
⊢ W = W' → dualAnnihilator W = dualAnnihilator W'
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W W' : Subspace K V
⊢ dualAnnihilator W = dualAnnihilator W' ↔ W = W'
constructor
no goals
case mp
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W W' : Subspace K V
⊢ dualAnnihilator W = dualAnnihilator W' → W = W'
apply (dualAnnihilatorGci K V).l_injective
case mpr
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
⊢ dualAnnihilator W = dualAnnihilator W
case mpr
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W W' : Subspace K V
⊢ W = W' → dualAnnihilator W = dualAnnihilator W'
rintro rfl
no goals
case mpr
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
⊢ dualAnnihilator W = dualAnnihilator W
rfl