Finiteness of products

instance Finite.instProd {α : Type u_1} {β : Type u_2} [Finite α] [Finite β] : Finite (α × β)

Equations

• ⋯ = ⋯

instance Finite.instPProd {α : Sort u_3} {β : Sort u_4} [Finite α] [Finite β] : Finite (α ×' β)

Equations

• ⋯ = ⋯

theorem Finite.prod_left {α : Type u_1} (β : Type u_3) [Finite (α × β)] [Nonempty β] : Finite α

theorem Finite.prod_right {β : Type u_2} (α : Type u_3) [Finite (α × β)] [Nonempty α] : Finite β

instance Pi.finite {α : Sort u_3} {β : α → Sort u_4} [Finite α] [∀ (a : α), Finite (β a)] : Finite ((a : α) → β a)

Equations

• ⋯ = ⋯

instance instFiniteSym {α : Type u_1} [Finite α] {n : ℕ} : Finite (Sym α n)

Equations

• ⋯ = ⋯

instance Function.Embedding.finite {α : Sort u_3} {β : Sort u_4} [Finite β] : Finite (α ↪ β)

Equations

• ⋯ = ⋯

instance Equiv.finite_right {α : Sort u_3} {β : Sort u_4} [Finite β] : Finite (α ≃ β)

Equations

• ⋯ = ⋯

instance Equiv.finite_left {α : Sort u_3} {β : Sort u_4} [Finite α] : Finite (α ≃ β)

Equations

• ⋯ = ⋯