case intro
R : Type ?u.1057928
inst✝¹¹ : CommRing R
M : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.1058519
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.1059061
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M
A✝ : Type ?u.1059539
inst✝⁴ : CommRing A✝
inst✝³ : Module A✝ M
κ : Type ?u.1060037
inst✝² : Fintype κ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Module A M
f : M →ₗ[A] M
hf : IsUnit f
g : M →ₗ[A] M
hg : comp f g = 1
⊢ IsUnit (↑LinearMap.det f)
R : Type ?u.1057928
inst✝¹¹ : CommRing R
M : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.1058519
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.1059061
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M
A✝ : Type ?u.1059539
inst✝⁴ : CommRing A✝
inst✝³ : Module A✝ M
κ : Type ?u.1060037
inst✝² : Fintype κ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Module A M
f : M →ₗ[A] M
hf : IsUnit f
⊢ IsUnit (↑LinearMap.det f)
obtain ⟨g, hg⟩ : ∃ g, f.comp g = 1 := hf.exists_right_inv
case intro
R : Type ?u.1057928
inst✝¹¹ : CommRing R
M : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.1058519
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.1059061
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M
A✝ : Type ?u.1059539
inst✝⁴ : CommRing A✝
inst✝³ : Module A✝ M
κ : Type ?u.1060037
inst✝² : Fintype κ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Module A M
f : M →ₗ[A] M
hf : IsUnit f
g : M →ₗ[A] M
hg : comp f g = 1
this : ↑LinearMap.det f * ↑LinearMap.det g = 1
⊢ IsUnit (↑LinearMap.det f)
case intro
R : Type ?u.1057928
inst✝¹¹ : CommRing R
M : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.1058519
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.1059061
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M
A✝ : Type ?u.1059539
inst✝⁴ : CommRing A✝
inst✝³ : Module A✝ M
κ : Type ?u.1060037
inst✝² : Fintype κ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Module A M
f : M →ₗ[A] M
hf : IsUnit f
g : M →ₗ[A] M
hg : comp f g = 1
⊢ IsUnit (↑LinearMap.det f)
have : LinearMap.det f * LinearMap.det g = 1 := by
  simp only [← LinearMap.det_comp, hg, MonoidHom.map_one]
no goals
case intro
R : Type ?u.1057928
inst✝¹¹ : CommRing R
M : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.1058519
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.1059061
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M
A✝ : Type ?u.1059539
inst✝⁴ : CommRing A✝
inst✝³ : Module A✝ M
κ : Type ?u.1060037
inst✝² : Fintype κ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Module A M
f : M →ₗ[A] M
hf : IsUnit f
g : M →ₗ[A] M
hg : comp f g = 1
this : ↑LinearMap.det f * ↑LinearMap.det g = 1
⊢ IsUnit (↑LinearMap.det f)
exact isUnit_of_mul_eq_one _ _ this
no goals
R : Type ?u.1057928
inst✝¹¹ : CommRing R
M : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.1058519
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.1059061
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M
A✝ : Type ?u.1059539
inst✝⁴ : CommRing A✝
inst✝³ : Module A✝ M
κ : Type ?u.1060037
inst✝² : Fintype κ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Module A M
f : M →ₗ[A] M
hf : IsUnit f
g : M →ₗ[A] M
hg : comp f g = 1
⊢ ↑LinearMap.det f * ↑LinearMap.det g = 1
simp only [← LinearMap.det_comp, hg, MonoidHom.map_one]