-
Definition orthogonal gT D S1 S2 :=
nosimpl (@
ortho_rec gT D S1 S2).
+
Definition orthogonal gT D S1 S2 :=
nosimpl (@
ortho_rec gT D S1 S2).
-
Notation "{ 'in' CFD , 'isometry' tau , 'to' CFR }" :=
- (
isometry_from_to (
mem CFD)
tau (
mem CFR))
+
Notation "{ 'in' CFD , 'isometry' tau , 'to' CFR }" :=
+ (
isometry_from_to (
mem CFD)
tau (
mem CFR))
(
at level 0,
format "{ 'in' CFD , 'isometry' tau , 'to' CFR }")
:
type_scope.
@@ -479,128 +478,128 @@
Section ClassFun.
-
Variables (
gT :
finGroupType) (
G :
{group gT}).
-
Implicit Types (
A B :
{set gT}) (
H K :
{group gT}) (
phi psi xi :
'CF(G)).
+
Variables (
gT :
finGroupType) (
G :
{group gT}).
+
Implicit Types (
A B :
{set gT}) (
H K :
{group gT}) (
phi psi xi :
'CF(G)).
-
Lemma cfun0 phi x :
x \notin G → phi x = 0.
+
Lemma cfun0 phi x :
x \notin G → phi x = 0.
-
Lemma support_cfun phi :
support phi \subset G.
+
Lemma support_cfun phi :
support phi \subset G.
-
Lemma cfunJ phi x y :
y \in G → phi (
x ^ y)
= phi x.
+
Lemma cfunJ phi x y :
y \in G → phi (
x ^ y)
= phi x.
-
Lemma cfun_repr phi x :
phi (
repr (
x ^: G))
= phi x.
+
Lemma cfun_repr phi x :
phi (
repr (
x ^: G))
= phi x.
-
Lemma cfun_inP phi psi :
{in G, phi =1 psi} → phi = psi.
+
Lemma cfun_inP phi psi :
{in G, phi =1 psi} → phi = psi.
-
Lemma cfuniE A x :
A <| G → '1_A x = (x \in A)%:R.
+
Lemma cfuniE A x :
A <| G → '1_A x = (x \in A)%:R.
-
Lemma support_cfuni A :
A <| G → support '1_A =i A.
+
Lemma support_cfuni A :
A <| G → support '1_A =i A.
-
Lemma eq_mul_cfuni A phi :
A <| G → {in A, phi × '1_A =1 phi}.
+
Lemma eq_mul_cfuni A phi :
A <| G → {in A, phi × '1_A =1 phi}.
-
Lemma eq_cfuni A :
A <| G → {in A, '1_A =1 (1
: 'CF(G))}.
+
Lemma eq_cfuni A :
A <| G → {in A, '1_A =1 (1
: 'CF(G))}.
-
Lemma cfuniG :
'1_G = 1.
+
Lemma cfuniG :
'1_G = 1.
-
Lemma cfun1E g : (1
: 'CF(G))
g = (g \in G)%:R.
+
Lemma cfun1E g : (1
: 'CF(G))
g = (g \in G)%:R.
-
Lemma cfun11 : (1
: 'CF(G)) 1%
g = 1.
+
Lemma cfun11 : (1
: 'CF(G)) 1%
g = 1.
-
Lemma prod_cfunE I r (
P :
pred I) (
phi :
I → 'CF(G))
x :
-
x \in G → (
\prod_(i <- r | P i) phi i)
x = \prod_(i <- r | P i) (
phi i)
x.
+
Lemma prod_cfunE I r (
P :
pred I) (
phi :
I → 'CF(G))
x :
+
x \in G → (
\prod_(i <- r | P i) phi i)
x = \prod_(i <- r | P i) (
phi i)
x.
-
Lemma exp_cfunE phi n x :
x \in G → (
phi ^+ n)
x = phi x ^+ n.
+
Lemma exp_cfunE phi n x :
x \in G → (
phi ^+ n)
x = phi x ^+ n.
-
Lemma mul_cfuni A B :
'1_A × '1_B = '1_(A :&: B) :> 'CF(G).
+
Lemma mul_cfuni A B :
'1_A × '1_B = '1_(A :&: B) :> 'CF(G).
-
Lemma cfun_classE x y :
'1_(x ^: G) y = ((x \in G) && (y \in x ^: G))%:R.
+
Lemma cfun_classE x y :
'1_(x ^: G) y = ((x \in G) && (y \in x ^: G))%:R.
Lemma cfun_on_sum A :
-
'CF(G, A) = (
\sum_(xG in classes G | xG \subset A) <['1_xG]>)%
VS.
+
'CF(G, A) = (
\sum_(xG in classes G | xG \subset A) <['1_xG]>)%
VS.
Lemma cfun_onP A phi :
-
reflect (
∀ x,
x \notin A → phi x = 0) (
phi \in 'CF(G, A)).
+
reflect (
∀ x,
x \notin A → phi x = 0) (
phi \in 'CF(G, A)).
-
Lemma cfun_on0 A phi x :
phi \in 'CF(G, A) → x \notin A → phi x = 0.
+
Lemma cfun_on0 A phi x :
phi \in 'CF(G, A) → x \notin A → phi x = 0.
-
Lemma sum_by_classes (
R :
ringType) (
F :
gT → R) :
-
{in G &, ∀ g h,
F (
g ^ h)
= F g} →
-
\sum_(g in G) F g = \sum_(xG in classes G) #|xG|%:R × F (
repr xG).
+
Lemma sum_by_classes (
R :
ringType) (
F :
gT → R) :
+
{in G &, ∀ g h,
F (
g ^ h)
= F g} →
+
\sum_(g in G) F g = \sum_(xG in classes G) #|xG|%:R × F (
repr xG).
Lemma cfun_base_free A :
free (
cfun_base G A).
-
Lemma dim_cfun :
\dim 'CF(G) = #|classes G|.
+
Lemma dim_cfun :
\dim 'CF(G) = #|classes G|.
-
Lemma dim_cfun_on A :
\dim 'CF(G, A) = #|classes G ::&: A|.
+
Lemma dim_cfun_on A :
\dim 'CF(G, A) = #|classes G ::&: A|.
-
Lemma dim_cfun_on_abelian A :
abelian G → A \subset G → \dim 'CF(G, A) = #|A|.
+
Lemma dim_cfun_on_abelian A :
abelian G → A \subset G → \dim 'CF(G, A) = #|A|.
-
Lemma cfuni_on A :
'1_A \in 'CF(G, A).
+
Lemma cfuni_on A :
'1_A \in 'CF(G, A).
-
Lemma mul_cfuni_on A phi :
phi × '1_A \in 'CF(G, A).
+
Lemma mul_cfuni_on A phi :
phi × '1_A \in 'CF(G, A).
-
Lemma cfun_onE phi A :
(phi \in 'CF(G, A)) = (support phi \subset A).
+
Lemma cfun_onE phi A :
(phi \in 'CF(G, A)) = (support phi \subset A).
-
Lemma cfun_onT phi :
phi \in 'CF(G, [set: gT]).
+
Lemma cfun_onT phi :
phi \in 'CF(G, [set: gT]).
Lemma cfun_onD1 phi A :
-
(phi \in 'CF(G, A^#)) = (phi \in 'CF(G, A)) && (phi 1%
g == 0
).
+
(phi \in 'CF(G, A^#)) = (phi \in 'CF(G, A)) && (phi 1%
g == 0
).
-
Lemma cfun_onG phi :
phi \in 'CF(G, G).
+
Lemma cfun_onG phi :
phi \in 'CF(G, G).
-
Lemma cfunD1E phi :
(phi \in 'CF(G, G^#)) = (phi 1%
g == 0
).
+
Lemma cfunD1E phi :
(phi \in 'CF(G, G^#)) = (phi 1%
g == 0
).
-
Lemma cfunGid :
'CF(G, G) = 'CF(G)%
VS.
+
Lemma cfunGid :
'CF(G, G) = 'CF(G)%
VS.
-
Lemma cfun_onS A B phi :
B \subset A → phi \in 'CF(G, B) → phi \in 'CF(G, A).
+
Lemma cfun_onS A B phi :
B \subset A → phi \in 'CF(G, B) → phi \in 'CF(G, A).
Lemma cfun_complement A :
-
A <| G → (
'CF(G, A) + 'CF(G, G :\: A)%
SET = 'CF(G))%
VS.
+
A <| G → (
'CF(G, A) + 'CF(G, G :\: A)%
SET = 'CF(G))%
VS.
-
Lemma cfConjCE phi x : (
phi^*)%
CF x = (phi x)^*.
+
Lemma cfConjCE phi x : (
phi^*)%
CF x = (phi x)^*.
-
Lemma cfConjCK :
involutive (
fun phi ⇒
phi^*)%
CF.
+
Lemma cfConjCK :
involutive (
fun phi ⇒
phi^*)%
CF.
-
Lemma cfConjC_cfun1 : (1
^*)%
CF = 1
:> 'CF(G).
+
Lemma cfConjC_cfun1 : (1
^*)%
CF = 1
:> 'CF(G).