R : Type ?u.365280
R₁ : Type ?u.365283
R₂ : Type ?u.365286
R₃ : Type ?u.365289
k : Type ?u.365292
S : Type ?u.365295
S₃ : Type ?u.365298
T : Type ?u.365301
M : Type u_1
M₁ : Type ?u.365307
M₂ : Type u_2
M₃ : Type ?u.365313
N₁ : Type ?u.365316
N₂ : Type ?u.365319
N₃ : Type ?u.365322
ι : Type ?u.365325
inst✝³ : AddCommGroup M
inst✝² : Module ℚ M
inst✝¹ : AddCommGroup M₂
inst✝ : Module ℚ M₂
f g : M →+ M₂
h : toRatLinearMap f = toRatLinearMap g
⊢ f = g
R : Type ?u.365280
R₁ : Type ?u.365283
R₂ : Type ?u.365286
R₃ : Type ?u.365289
k : Type ?u.365292
S : Type ?u.365295
S₃ : Type ?u.365298
T : Type ?u.365301
M : Type u_1
M₁ : Type ?u.365307
M₂ : Type u_2
M₃ : Type ?u.365313
N₁ : Type ?u.365316
N₂ : Type ?u.365319
N₃ : Type ?u.365322
ι : Type ?u.365325
inst✝³ : AddCommGroup M
inst✝² : Module ℚ M
inst✝¹ : AddCommGroup M₂
inst✝ : Module ℚ M₂
⊢ Injective toRatLinearMap
intro f g h
case h
R : Type ?u.365280
R₁ : Type ?u.365283
R₂ : Type ?u.365286
R₃ : Type ?u.365289
k : Type ?u.365292
S : Type ?u.365295
S₃ : Type ?u.365298
T : Type ?u.365301
M : Type u_1
M₁ : Type ?u.365307
M₂ : Type u_2
M₃ : Type ?u.365313
N₁ : Type ?u.365316
N₂ : Type ?u.365319
N₃ : Type ?u.365322
ι : Type ?u.365325
inst✝³ : AddCommGroup M
inst✝² : Module ℚ M
inst✝¹ : AddCommGroup M₂
inst✝ : Module ℚ M₂
f g : M →+ M₂
h : toRatLinearMap f = toRatLinearMap g
x : M
⊢ ↑f x = ↑g x
R : Type ?u.365280
R₁ : Type ?u.365283
R₂ : Type ?u.365286
R₃ : Type ?u.365289
k : Type ?u.365292
S : Type ?u.365295
S₃ : Type ?u.365298
T : Type ?u.365301
M : Type u_1
M₁ : Type ?u.365307
M₂ : Type u_2
M₃ : Type ?u.365313
N₁ : Type ?u.365316
N₂ : Type ?u.365319
N₃ : Type ?u.365322
ι : Type ?u.365325
inst✝³ : AddCommGroup M
inst✝² : Module ℚ M
inst✝¹ : AddCommGroup M₂
inst✝ : Module ℚ M₂
f g : M →+ M₂
h : toRatLinearMap f = toRatLinearMap g
⊢ f = g
ext x
no goals
case h
R : Type ?u.365280
R₁ : Type ?u.365283
R₂ : Type ?u.365286
R₃ : Type ?u.365289
k : Type ?u.365292
S : Type ?u.365295
S₃ : Type ?u.365298
T : Type ?u.365301
M : Type u_1
M₁ : Type ?u.365307
M₂ : Type u_2
M₃ : Type ?u.365313
N₁ : Type ?u.365316
N₂ : Type ?u.365319
N₃ : Type ?u.365322
ι : Type ?u.365325
inst✝³ : AddCommGroup M
inst✝² : Module ℚ M
inst✝¹ : AddCommGroup M₂
inst✝ : Module ℚ M₂
f g : M →+ M₂
h : toRatLinearMap f = toRatLinearMap g
x : M
⊢ ↑f x = ↑g x
exact LinearMap.congr_fun h x