Theorems · Theorem · commutative algebra

Module.Basis.ofSplitExact.congr_simp

∀ {R : Type u_1} {M : Type u_2} {K : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup K] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R K] [inst_6 : Module R P]
  {f f_1 : K →ₗ[R] M} (e_f : f = f_1) {g g_1 : M →ₗ[R] P} (e_g : g = g_1) {s s_1 : M →ₗ[R] K} (e_s : s = s_1)
  (hs : s ∘ₗ f = LinearMap.id) (hfg : Function.Exact ⇑f ⇑g) {ι : Type u_5} {κ : Type u_6} {σ : Type u_7} {a a_1 : κ → ι}
  (e_a : a = a_1) {b b_1 : σ → ι} (e_b : b = b_1) (hg : Function.Surjective ⇑g) (v v_1 : Module.Basis ι R M)
  (e_v : v = v_1) (hainj : Function.Injective a) (hsa : ∀ (i : κ), s (v (a i)) = 0)
  (hlib : LinearIndependent R (⇑s ∘ ⇑v ∘ b)) (hab : Codisjoint (Set.range a) (Set.range b)),
  Module.Basis.ofSplitExact hs hfg hg v hainj hsa hlib hab = Module.Basis.ofSplitExact ⋯ ⋯ ⋯ v_1 ⋯ ⋯ ⋯ ⋯

Defined in

Mathlib.RingTheory.Smooth.StandardSmoothCotangent

Cited by

0 results in Mathlib

Foundations

Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingAddCommGroupAddCommGroupAddCommGroupModuleModuleModule