LeanPool.BruhatTits.Utils.Misc

theorem lambda_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → γ) : ((fun (b : β) => g b) ∘ fun (a : α) => f a) = g ∘ f

theorem exp_le_exp_of_pow_le_pow {Γ₀ : Type u_4} [LinearOrderedCommGroupWithZero Γ₀] (a : Γ₀) (hlt : a < 1) (h₀ : a ≠ 0) {n m : ℤ} (hle : a ^ n ≤ a ^ m) : m ≤ n

theorem exp_zero_of_pow_eq_one_aux {Γ₀ : Type u_4} [LinearOrderedCommGroupWithZero Γ₀] {n : ℕ} (ha : 0 ^ n = 1) : n = 0

theorem exp_zero_of_zpow_eq_one' {Γ₀ : Type u_4} [LinearOrderedCommGroupWithZero Γ₀] {n : ℤ} (ha : 0 ^ n = 1) : n = 0

theorem exp_zero_of_zpow_eq_one {Γ₀ : Type u_4} [LinearOrderedCommGroupWithZero Γ₀] {a : Γ₀} (h : a < 1) {n : ℤ} (han : a ^ n = 1) : n = 0

theorem Pi.basisFun_eq_single {ι : Type u_5} [Finite ι] [DecidableEq ι] {R : Type u_6} [Semiring R] (i : ι) : (basisFun R ι) i = single i 1

@[simp]

theorem Matrix.GeneralLinearGroup.toLinear_symm_ofLinearEquiv_apply {ι : Type u_5} [DecidableEq ι] [Fintype ι] {R : Type u_6} [CommRing R] (e : (ι → R) ≃ₗ[R] ι → R) (i j : ι) : ↑(toLin.symm (LinearMap.GeneralLinearGroup.ofLinearEquiv e)) i j = e (Pi.single j 1) i

theorem Fin.rev_antitone (n : ℕ) : Antitone rev

theorem Finset.prod_zpow_eq_zpow_sum {ι : Type u_5} {β : Type u_7} [CommGroupWithZero β] (s : Finset ι) (f : ι → ℤ) (a : β) (ha : a ≠ 0) : ∏ i ∈ s, a ^ f i = a ^ ∑ i ∈ s, f i

theorem IsLocalRing.exists_isUnit_of_isUnit_sum {ι : Type u_5} {R : Type u_6} [CommRing R] [IsLocalRing R] {s : Finset ι} {f : ι → R} (h : IsUnit (∑ i ∈ s, f i)) : ∃ i ∈ s, IsUnit (f i)

def Fin.succEquivUnit (n : ℕ) : Fin (n + 1) ≃ Fin n ⊕ Unit

Fin (n + 1) is equivalent to Fin n ⊕ Unit.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Fin.succEquivUnit_symm_apply (n : ℕ) (a✝ : Fin n ⊕ Unit) : (succEquivUnit n).symm a✝ = Sum.elim (fun (j : Fin n) => j.castSucc) (fun (x : Unit) => last n) a✝

@[simp]

theorem Fin.succEquivUnit_apply (n : ℕ) (j : Fin (n + 1)) : (succEquivUnit n) j = if h : ↑j < n then Sum.inl ⟨↑j, h⟩ else Sum.inr ()

theorem MulAction.stabilizer_fun_const {α : Type u_5} (ι : Type u_6) (G : Type u_7) [Nonempty ι] [Group G] [MulAction G α] (x : α) : (stabilizer G fun (x_1 : ι) => x) = stabilizer G x

theorem MulAction.stabilizer_pi {ι : Type u_5} {α : ι → Type u_6} (G : Type u_7) [Group G] [(i : ι) → MulAction G (α i)] (x : (i : ι) → α i) : stabilizer G x = ⨅ (i : ι), stabilizer G (x i)

theorem MulAction.mem_stabilizer_pi {ι : Type u_5} {α : ι → Type u_6} {G : Type u_7} [Group G] [(i : ι) → MulAction G (α i)] (x : (i : ι) → α i) (g : G) : g ∈ stabilizer G x ↔ ∀ (i : ι), g ∈ stabilizer G (x i)