ι : Type u_1
R : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsPrincipalIdealRing R
M : Type ?u.391806
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
b✝ : ι → M
S : Type u_3
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
i : ι
hi : smithCoeffs b I hI i = 0
⊢ False
ι : Type u_1
R : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsPrincipalIdealRing R
M : Type ?u.391806
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
b✝ : ι → M
S : Type u_3
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
i : ι
⊢ smithCoeffs b I hI i ≠ 0
intro hi
ι : Type u_1
R : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsPrincipalIdealRing R
M : Type ?u.391806
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
b✝ : ι → M
S : Type u_3
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
i : ι
hi : smithCoeffs b I hI i = 0
⊢ ↑(selfBasis b I hI) i = 0
ι : Type u_1
R : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsPrincipalIdealRing R
M : Type ?u.391806
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
b✝ : ι → M
S : Type u_3
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
i : ι
hi : smithCoeffs b I hI i = 0
⊢ False
apply Basis.ne_zero (Ideal.selfBasis b I hI) i
ι : Type u_1
R : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsPrincipalIdealRing R
M : Type ?u.391806
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
b✝ : ι → M
S : Type u_3
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
i : ι
hi : smithCoeffs b I hI i = 0
⊢ (fun a => ↑a) (↑(selfBasis b I hI) i) = (fun a => ↑a) 0
ι : Type u_1
R : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsPrincipalIdealRing R
M : Type ?u.391806
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
b✝ : ι → M
S : Type u_3
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
i : ι
hi : smithCoeffs b I hI i = 0
⊢ ↑(selfBasis b I hI) i = 0
refine' Subtype.coe_injective _
no goals
ι : Type u_1
R : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsPrincipalIdealRing R
M : Type ?u.391806
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
b✝ : ι → M
S : Type u_3
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
i : ι
hi : smithCoeffs b I hI i = 0
⊢ (fun a => ↑a) (↑(selfBasis b I hI) i) = (fun a => ↑a) 0
simp [hi]