case zero
R : Type u
S : Type ?u.1021136
σ : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
D : Type u
inst✝³ : CommRing D
inst✝² : IsDomain D
inst✝¹ : UniqueFactorizationMonoid D
d : ℕ
inst✝ : Fintype σ
⊢ UniqueFactorizationMonoid (MvPolynomial (Fin Nat.zero) D)

case succ
R : Type u
S : Type ?u.1021136
σ : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
D : Type u
inst✝³ : CommRing D
inst✝² : IsDomain D
inst✝¹ : UniqueFactorizationMonoid D
d✝ : ℕ
inst✝ : Fintype σ
d : ℕ
hd : UniqueFactorizationMonoid (MvPolynomial (Fin d) D)
⊢ UniqueFactorizationMonoid (MvPolynomial (Fin (Nat.succ d)) D)
R : Type u
S : Type ?u.1021136
σ : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
D : Type u
inst✝³ : CommRing D
inst✝² : IsDomain D
inst✝¹ : UniqueFactorizationMonoid D
d : ℕ
inst✝ : Fintype σ
⊢ UniqueFactorizationMonoid (MvPolynomial (Fin (Fintype.card σ)) D)
induction' Fintype.card σ with d hd
case zero
R : Type u
S : Type ?u.1021136
σ : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
D : Type u
inst✝³ : CommRing D
inst✝² : IsDomain D
inst✝¹ : UniqueFactorizationMonoid D
d : ℕ
inst✝ : Fintype σ
⊢ UniqueFactorizationMonoid D
case zero
R : Type u
S : Type ?u.1021136
σ : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
D : Type u
inst✝³ : CommRing D
inst✝² : IsDomain D
inst✝¹ : UniqueFactorizationMonoid D
d : ℕ
inst✝ : Fintype σ
⊢ UniqueFactorizationMonoid (MvPolynomial (Fin Nat.zero) D)
apply (isEmptyAlgEquiv D (Fin 0)).toMulEquiv.symm.uniqueFactorizationMonoid
no goals
case zero
R : Type u
S : Type ?u.1021136
σ : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
D : Type u
inst✝³ : CommRing D
inst✝² : IsDomain D
inst✝¹ : UniqueFactorizationMonoid D
d : ℕ
inst✝ : Fintype σ
⊢ UniqueFactorizationMonoid D
infer_instance
case succ
R : Type u
S : Type ?u.1021136
σ : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
D : Type u
inst✝³ : CommRing D
inst✝² : IsDomain D
inst✝¹ : UniqueFactorizationMonoid D
d✝ : ℕ
inst✝ : Fintype σ
d : ℕ
hd : UniqueFactorizationMonoid (MvPolynomial (Fin d) D)
⊢ UniqueFactorizationMonoid (MvPolynomial (Fin (d + 1)) D)
case succ
R : Type u
S : Type ?u.1021136
σ : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
D : Type u
inst✝³ : CommRing D
inst✝² : IsDomain D
inst✝¹ : UniqueFactorizationMonoid D
d✝ : ℕ
inst✝ : Fintype σ
d : ℕ
hd : UniqueFactorizationMonoid (MvPolynomial (Fin d) D)
⊢ UniqueFactorizationMonoid (MvPolynomial (Fin (Nat.succ d)) D)
rw [Nat.succ_eq_add_one d]
case succ.e
R : Type u
S : Type ?u.1021136
σ : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
D : Type u
inst✝³ : CommRing D
inst✝² : IsDomain D
inst✝¹ : UniqueFactorizationMonoid D
d✝ : ℕ
inst✝ : Fintype σ
d : ℕ
hd : UniqueFactorizationMonoid (MvPolynomial (Fin d) D)
⊢ ?m.1023575 ≃* MvPolynomial (Fin (d + 1)) D

case succ.hα
R : Type u
S : Type ?u.1021136
σ : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
D : Type u
inst✝³ : CommRing D
inst✝² : IsDomain D
inst✝¹ : UniqueFactorizationMonoid D
d✝ : ℕ
inst✝ : Fintype σ
d : ℕ
hd : UniqueFactorizationMonoid (MvPolynomial (Fin d) D)
⊢ UniqueFactorizationMonoid ?m.1023575

R : Type u
S : Type ?u.1021136
σ : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
D : Type u
inst✝³ : CommRing D
inst✝² : IsDomain D
inst✝¹ : UniqueFactorizationMonoid D
d✝ : ℕ
inst✝ : Fintype σ
d : ℕ
hd : UniqueFactorizationMonoid (MvPolynomial (Fin d) D)
⊢ Type ?u.1023573

R : Type u
S : Type ?u.1021136
σ : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
D : Type u
inst✝³ : CommRing D
inst✝² : IsDomain D
inst✝¹ : UniqueFactorizationMonoid D
d✝ : ℕ
inst✝ : Fintype σ
d : ℕ
hd : UniqueFactorizationMonoid (MvPolynomial (Fin d) D)
⊢ CancelCommMonoidWithZero ?m.1023575
case succ
R : Type u
S : Type ?u.1021136
σ : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
D : Type u
inst✝³ : CommRing D
inst✝² : IsDomain D
inst✝¹ : UniqueFactorizationMonoid D
d✝ : ℕ
inst✝ : Fintype σ
d : ℕ
hd : UniqueFactorizationMonoid (MvPolynomial (Fin d) D)
⊢ UniqueFactorizationMonoid (MvPolynomial (Fin (d + 1)) D)
apply @MulEquiv.uniqueFactorizationMonoid _ _ (_) (_)
no goals
case succ.e
R : Type u
S : Type ?u.1021136
σ : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
D : Type u
inst✝³ : CommRing D
inst✝² : IsDomain D
inst✝¹ : UniqueFactorizationMonoid D
d✝ : ℕ
inst✝ : Fintype σ
d : ℕ
hd : UniqueFactorizationMonoid (MvPolynomial (Fin d) D)
⊢ ?m.1023575 ≃* MvPolynomial (Fin (d + 1)) D
exact (finSuccEquiv D d).toMulEquiv.symm
R : Type u
S : Type ?u.1021136
σ : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
D : Type u
inst✝³ : CommRing D
inst✝² : IsDomain D
inst✝¹ : UniqueFactorizationMonoid D
d✝ : ℕ
inst✝ : Fintype σ
d : ℕ
hd : UniqueFactorizationMonoid (MvPolynomial (Fin d) D)
⊢ UniqueFactorizationMonoid (MvPolynomial (Fin d) D)
case succ.hα
R : Type u
S : Type ?u.1021136
σ : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
D : Type u
inst✝³ : CommRing D
inst✝² : IsDomain D
inst✝¹ : UniqueFactorizationMonoid D
d✝ : ℕ
inst✝ : Fintype σ
d : ℕ
hd : UniqueFactorizationMonoid (MvPolynomial (Fin d) D)
⊢ UniqueFactorizationMonoid (MvPolynomial (Fin d) D)[X]
apply @Polynomial.uniqueFactorizationMonoid (MvPolynomial (Fin d) D) _ _ ?_
no goals
R : Type u
S : Type ?u.1021136
σ : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
D : Type u
inst✝³ : CommRing D
inst✝² : IsDomain D
inst✝¹ : UniqueFactorizationMonoid D
d✝ : ℕ
inst✝ : Fintype σ
d : ℕ
hd : UniqueFactorizationMonoid (MvPolynomial (Fin d) D)
⊢ UniqueFactorizationMonoid (MvPolynomial (Fin d) D)
assumption